P (lemma)
pair_sp [in Coq.IntMap.Mapiter]
paradox [in Coq.Logic.Hurkens]
pascal [in Coq.Reals.Binomial]
pascal_step1 [in Coq.Reals.Binomial]
pascal_step2 [in Coq.Reals.Binomial]
pascal_step3 [in Coq.Reals.Binomial]
Pcase [in Coq.NArith.BinPos]
Pcompare_antisym [in Coq.NArith.BinPos]
Pcompare_Eq_eq [in Coq.NArith.BinPos]
Pcompare_Gt_Gt [in Coq.NArith.BinPos]
Pcompare_Gt_Lt [in Coq.NArith.BinPos]
Pcompare_Lt_Gt [in Coq.NArith.BinPos]
Pcompare_Lt_Lt [in Coq.NArith.BinPos]
Pcompare_minus_l [in Coq.NArith.Pnat]
Pcompare_minus_r [in Coq.NArith.Pnat]
Pcompare_not_Eq [in Coq.NArith.BinPos]
Pcompare_refl [in Coq.NArith.BinPos]
Pdiv2 [in Coq.ZArith.Zbinary]
Pdouble_minus_one_o_succ_eq_xI [in Coq.NArith.BinPos]
permut_app [in Coq.Sorting.Permutation]
permut_cons [in Coq.Sorting.Permutation]
permut_middle [in Coq.Sorting.Permutation]
permut_refl [in Coq.Sorting.Permutation]
permut_right [in Coq.Sorting.Permutation]
permut_tran [in Coq.Sorting.Permutation]
perm_left [in Coq.Sets.Permut]
perm_right [in Coq.Sets.Permut]
phi_sequence_prop [in Coq.Reals.RiemannInt]
Pigeonhole [in Coq.Sets.Image]
Pigeonhole_bis [in Coq.Sets.Infinite_sets]
Pigeonhole_principle [in Coq.Sets.Image]
Pigeonhole_ter [in Coq.Sets.Infinite_sets]
Pind [in Coq.NArith.BinPos]
PI2_RGT_0 [in Coq.Reals.Rtrigo]
PI2_Rlt_PI [in Coq.Reals.Rtrigo]
PI4_RGT_0 [in Coq.Reals.Rtrigo_calc]
PI4_RLT_PI2 [in Coq.Reals.Rtrigo]
PI6_RGT_0 [in Coq.Reals.Rtrigo_calc]
PI6_RLT_PI2 [in Coq.Reals.Rtrigo_calc]
PI_ineq [in Coq.Reals.AltSeries]
PI_neq0 [in Coq.Reals.Rtrigo]
PI_RGT_0 [in Coq.Reals.AltSeries]
PI_tg_cv [in Coq.Reals.AltSeries]
PI_tg_decreasing [in Coq.Reals.AltSeries]
PI_tg_pos [in Coq.Reals.AltSeries]
PI_4 [in Coq.Reals.Rtrigo_alt]
plus_assoc [in Coq.Arith.Plus]
plus_assoc_reverse [in Coq.Arith.Plus]
plus_comm [in Coq.Arith.Plus]
plus_frac_part1 [in Coq.Reals.R_Ifp]
plus_frac_part2 [in Coq.Reals.R_Ifp]
plus_gt_compat_l [in Coq.Arith.Gt]
plus_gt_reg_l [in Coq.Arith.Gt]
plus_INR [in Coq.Reals.RIneq]
plus_Int_part1 [in Coq.Reals.R_Ifp]
plus_Int_part2 [in Coq.Reals.R_Ifp]
plus_is_O [in Coq.Arith.Plus]
plus_iter_eq_plus [in Coq.NArith.BinPos]
plus_iter_xI [in Coq.NArith.BinPos]
plus_iter_xO [in Coq.NArith.BinPos]
plus_IZR [in Coq.Reals.RIneq]
plus_IZR_NEG_POS [in Coq.Reals.RIneq]
plus_le_compat [in Coq.Arith.Plus]
plus_le_compat_l [in Coq.Arith.Plus]
plus_le_compat_r [in Coq.Arith.Plus]
plus_le_is_le [in Coq.Reals.RIneq]
plus_le_lt_compat [in Coq.Arith.Plus]
plus_le_reg_l [in Coq.Arith.Plus]
plus_lt_compat [in Coq.Arith.Plus]
plus_lt_compat_l [in Coq.Arith.Plus]
plus_lt_compat_r [in Coq.Arith.Plus]
plus_lt_is_lt [in Coq.Reals.RIneq]
plus_lt_le_compat [in Coq.Arith.Plus]
plus_lt_reg_l [in Coq.Arith.Plus]
plus_minus [in Coq.Arith.Minus]
plus_n_O [in Coq.Init.Peano]
plus_n_Sm [in Coq.Init.Peano]
plus_O_n [in Coq.Init.Peano]
plus_permute [in Coq.Arith.Plus]
plus_permute_2_in_4 [in Coq.Arith.Plus]
plus_reg_l [in Coq.Arith.Plus]
plus_Snm_nSm [in Coq.Arith.Plus]
plus_Sn_m [in Coq.Init.Peano]
plus_sum [in Coq.Reals.PartSum]
plus_tail_plus [in Coq.Arith.Plus]
plus_0_l [in Coq.Arith.Plus]
plus_0_r [in Coq.Arith.Plus]
Pminus_mask_diag [in Coq.NArith.BinPos]
Pminus_mask_Gt [in Coq.NArith.BinPos]
Pmult_assoc [in Coq.NArith.BinPos]
Pmult_comm [in Coq.NArith.BinPos]
Pmult_minus_distr_l [in Coq.NArith.Pnat]
Pmult_nat_l_plus_morphism [in Coq.NArith.Pnat]
Pmult_nat_mult_permute [in Coq.NArith.Pnat]
Pmult_nat_plus_carry_morphism [in Coq.NArith.Pnat]
Pmult_nat_r_plus_morphism [in Coq.NArith.Pnat]
Pmult_nat_succ_morphism [in Coq.NArith.Pnat]
Pmult_nat_2_mult_2_permute [in Coq.NArith.Pnat]
Pmult_nat_4_mult_2_permute [in Coq.NArith.Pnat]
Pmult_plus_distr_l [in Coq.NArith.BinPos]
Pmult_plus_distr_r [in Coq.NArith.BinPos]
Pmult_reg_l [in Coq.NArith.BinPos]
Pmult_reg_r [in Coq.NArith.BinPos]
Pmult_xI_mult_xO_discr [in Coq.NArith.BinPos]
Pmult_xI_permute_r [in Coq.NArith.BinPos]
Pmult_xO_discr [in Coq.NArith.BinPos]
Pmult_xO_permute_r [in Coq.NArith.BinPos]
Pmult_1_inversion_l [in Coq.NArith.BinPos]
Pmult_1_r [in Coq.NArith.BinPos]
poly [in Coq.Reals.Rfunctions]
positive_derivative [in Coq.Reals.MVT]
pos_INR [in Coq.Reals.RIneq]
pos_Rl_P1 [in Coq.Reals.RList]
pos_Rl_P2 [in Coq.Reals.RList]
powerRZ_add [in Coq.Reals.Rfunctions]
powerRZ_le [in Coq.Reals.Rfunctions]
powerRZ_lt [in Coq.Reals.Rfunctions]
powerRZ_NOR [in Coq.Reals.Rfunctions]
powerRZ_O [in Coq.Reals.Rfunctions]
powerRZ_R1 [in Coq.Reals.Rfunctions]
powerRZ_1 [in Coq.Reals.Rfunctions]
Power_monotonic [in Coq.Reals.Rfunctions]
Power_set_Inhabited [in Coq.Sets.Powerset]
pow1 [in Coq.Reals.Rfunctions]
pow_add [in Coq.Reals.Rfunctions]
pow_i [in Coq.Reals.Rtrigo_def]
pow_incr [in Coq.Reals.Rfunctions]
pow_le [in Coq.Reals.Rfunctions]
pow_lt [in Coq.Reals.Rfunctions]
pow_lt_1_zero [in Coq.Reals.Rfunctions]
pow_maj_Rabs [in Coq.Reals.Rfunctions]
pow_mult [in Coq.Reals.Rfunctions]
pow_ne_zero [in Coq.Reals.Rfunctions]
pow_nonzero [in Coq.Reals.Rfunctions]
pow_O [in Coq.Reals.Rfunctions]
pow_Rabs [in Coq.Reals.Rfunctions]
pow_RN_plus [in Coq.Reals.Rfunctions]
pow_Rsqr [in Coq.Reals.Rfunctions]
pow_R1 [in Coq.Reals.Rfunctions]
pow_R1_Rle [in Coq.Reals.Rfunctions]
pow_sqr [in Coq.Reals.Cos_rel]
Pow_x_infinity [in Coq.Reals.Rfunctions]
pow_1 [in Coq.Reals.Rfunctions]
pow_1_abs [in Coq.Reals.Rfunctions]
pow_1_even [in Coq.Reals.Rfunctions]
pow_1_odd [in Coq.Reals.Rfunctions]
pow_2_n_growing [in Coq.Reals.Rsqrt_def]
pow_2_n_infty [in Coq.Reals.Rsqrt_def]
pow_2_n_neq_R0 [in Coq.Reals.Rsqrt_def]
Pplus_assoc [in Coq.NArith.BinPos]
Pplus_carry_no_neutral [in Coq.NArith.BinPos]
Pplus_carry_plus [in Coq.NArith.BinPos]
Pplus_carry_pred_eq_plus [in Coq.NArith.BinPos]
Pplus_carry_reg_l [in Coq.NArith.BinPos]
Pplus_carry_reg_r [in Coq.NArith.BinPos]
Pplus_carry_spec [in Coq.NArith.BinPos]
Pplus_comm [in Coq.NArith.BinPos]
Pplus_diag [in Coq.NArith.BinPos]
Pplus_minus [in Coq.NArith.BinPos]
Pplus_no_neutral [in Coq.NArith.BinPos]
Pplus_one_succ_l [in Coq.NArith.BinPos]
Pplus_one_succ_r [in Coq.NArith.BinPos]
Pplus_reg_l [in Coq.NArith.BinPos]
Pplus_reg_r [in Coq.NArith.BinPos]
Pplus_succ_permute_l [in Coq.NArith.BinPos]
Pplus_succ_permute_r [in Coq.NArith.BinPos]
Pplus_xI_double_minus_one [in Coq.NArith.BinPos]
Pplus_xO_double_minus_one [in Coq.NArith.BinPos]
Ppred_succ [in Coq.NArith.BinPos]
pred_ext_and_rel_choice_imp_EM [in Coq.Logic.Diaconescu]
pred_of_minus [in Coq.Arith.Minus]
pred_o_P_of_succ_nat_o_nat_of_P_eq_id [in Coq.NArith.Pnat]
pred_Sn [in Coq.Init.Peano]
prime_divisors [in Coq.ZArith.Znumtheory]
prime_mult [in Coq.ZArith.Znumtheory]
prime_rel_prime [in Coq.ZArith.Znumtheory]
prod_neq_R0 [in Coq.Reals.RIneq]
prod_SO_pos [in Coq.Reals.Rprod]
prod_SO_Rle [in Coq.Reals.Rprod]
prod_SO_split [in Coq.Reals.Rprod]
proj1 [in Coq.Init.Logic]
proj2 [in Coq.Init.Logic]
prolongement_C0 [in Coq.Reals.Rtopology]
proof_irrel [in Coq.Logic.Diaconescu]
proof_irrelevance [in Coq.Logic.Classical_Prop]
proof_irrelevance_cc [in Coq.Logic.ProofIrrelevance]
proof_irrelevance_cci [in Coq.Logic.ProofIrrelevance]
prop_degen_em [in Coq.Logic.ClassicalFacts]
prop_degen_ext [in Coq.Logic.ClassicalFacts]
prop_eps [in Coq.Reals.Rlimit]
prop_ext [in Coq.Logic.Diaconescu]
prop_ext_A_eq_A_imp_A [in Coq.Logic.ClassicalFacts]
prop_ext_em_degen [in Coq.Logic.ClassicalFacts]
prop_ext_retract_A_A_imp_A [in Coq.Logic.ClassicalFacts]
pr_nu [in Coq.Reals.Ranalysis1]
pr_nu_var [in Coq.Reals.Ranalysis4]
pr_nu_var2 [in Coq.Reals.Ranalysis4]
Psucc_discr [in Coq.NArith.BinPos]
Psucc_inj [in Coq.NArith.BinPos]
Psucc_not_one [in Coq.NArith.BinPos]
Psucc_o_double_minus_one_eq_xO [in Coq.NArith.BinPos]
Psucc_pred [in Coq.NArith.BinPos]
p2p1 [in Coq.Logic.ProofIrrelevance]
p2p2 [in Coq.Logic.ProofIrrelevance]
P_of_succ_nat_o_nat_of_P_eq_succ [in Coq.NArith.Pnat]
P_Rmin [in Coq.Reals.Rpower]
This page has been generated by coqdoc