P
pair [constructor, in Coq.Init.Datatypes]
pairT [constructor, in Coq.Init.Logic_Type]
pair_sp [lemma, in Coq.IntMap.Mapiter]
paradox [lemma, in Coq.Logic.Hurkens]
ParamDefiniteDescription [definition, in Coq.Logic.ChoiceFacts]
Partial_Order [library]
PartSum [library]
pascal [lemma, in Coq.Reals.Binomial]
pascal_step1 [lemma, in Coq.Reals.Binomial]
pascal_step2 [lemma, in Coq.Reals.Binomial]
pascal_step3 [lemma, in Coq.Reals.Binomial]
Pcase [lemma, in Coq.NArith.BinPos]
Pcompare [definition, in Coq.NArith.BinPos]
Pcompare [definition, in Coq.Arith.Compare]
Pcompare_antisym [lemma, in Coq.NArith.BinPos]
Pcompare_Eq_eq [lemma, in Coq.NArith.BinPos]
Pcompare_Gt_Gt [lemma, in Coq.NArith.BinPos]
Pcompare_Gt_Lt [lemma, in Coq.NArith.BinPos]
Pcompare_Lt_Gt [lemma, in Coq.NArith.BinPos]
Pcompare_Lt_Lt [lemma, in Coq.NArith.BinPos]
Pcompare_minus_l [lemma, in Coq.NArith.Pnat]
Pcompare_minus_r [lemma, in Coq.NArith.Pnat]
Pcompare_not_Eq [lemma, in Coq.NArith.BinPos]
Pcompare_refl [lemma, in Coq.NArith.BinPos]
Pdiv2 [definition, in Coq.NArith.BinPos]
Pdiv2 [lemma, in Coq.ZArith.Zbinary]
Pdouble_mask [definition, in Coq.NArith.BinPos]
Pdouble_minus_one [definition, in Coq.NArith.BinPos]
Pdouble_minus_one_o_succ_eq_xI [lemma, in Coq.NArith.BinPos]
Pdouble_minus_two [definition, in Coq.NArith.BinPos]
Pdouble_plus_one_mask [definition, in Coq.NArith.BinPos]
Peano [library]
Peano_dec [library]
PER [inductive, in Coq.Sets.Relations_1]
PER [inductive, in Coq.Relations.Relation_Definitions]
Permut [library]
permutation [definition, in Coq.Sorting.Permutation]
Permutation [library]
permut_app [lemma, in Coq.Sorting.Permutation]
permut_cons [lemma, in Coq.Sorting.Permutation]
permut_middle [lemma, in Coq.Sorting.Permutation]
permut_refl [lemma, in Coq.Sorting.Permutation]
permut_right [lemma, in Coq.Sorting.Permutation]
permut_tran [lemma, in Coq.Sorting.Permutation]
perm_left [lemma, in Coq.Sets.Permut]
perm_right [lemma, in Coq.Sets.Permut]
phi_sequence [definition, in Coq.Reals.RiemannInt]
phi_sequence_prop [lemma, in Coq.Reals.RiemannInt]
PI [definition, in Coq.Reals.AltSeries]
Pigeonhole [lemma, in Coq.Sets.Image]
Pigeonhole_bis [lemma, in Coq.Sets.Infinite_sets]
Pigeonhole_principle [lemma, in Coq.Sets.Image]
Pigeonhole_ter [lemma, in Coq.Sets.Infinite_sets]
Pind [lemma, in Coq.NArith.BinPos]
PI2_RGT_0 [lemma, in Coq.Reals.Rtrigo]
PI2_Rlt_PI [lemma, in Coq.Reals.Rtrigo]
PI4_RGT_0 [lemma, in Coq.Reals.Rtrigo_calc]
PI4_RLT_PI2 [lemma, in Coq.Reals.Rtrigo]
PI6_RGT_0 [lemma, in Coq.Reals.Rtrigo_calc]
PI6_RLT_PI2 [lemma, in Coq.Reals.Rtrigo_calc]
PI_ineq [lemma, in Coq.Reals.AltSeries]
PI_neq0 [lemma, in Coq.Reals.Rtrigo]
PI_RGT_0 [lemma, in Coq.Reals.AltSeries]
PI_tg [definition, in Coq.Reals.AltSeries]
PI_tg_cv [lemma, in Coq.Reals.AltSeries]
PI_tg_decreasing [lemma, in Coq.Reals.AltSeries]
PI_tg_pos [lemma, in Coq.Reals.AltSeries]
PI_4 [lemma, in Coq.Reals.Rtrigo_alt]
plat [definition, in Coq.Reals.Rtrigo_calc]
plus [definition, in Coq.Init.Peano]
Plus [library]
plus_acc [definition, in Coq.Arith.Plus]
plus_assoc [lemma, in Coq.Arith.Plus]
plus_assoc_reverse [lemma, in Coq.Arith.Plus]
plus_comm [lemma, in Coq.Arith.Plus]
plus_fct [definition, in Coq.Reals.Ranalysis1]
plus_frac_part1 [lemma, in Coq.Reals.R_Ifp]
plus_frac_part2 [lemma, in Coq.Reals.R_Ifp]
plus_gt_compat_l [lemma, in Coq.Arith.Gt]
plus_gt_reg_l [lemma, in Coq.Arith.Gt]
plus_INR [lemma, in Coq.Reals.RIneq]
plus_Int_part1 [lemma, in Coq.Reals.R_Ifp]
plus_Int_part2 [lemma, in Coq.Reals.R_Ifp]
plus_is_O [lemma, in Coq.Arith.Plus]
plus_is_one [definition, in Coq.Arith.Plus]
plus_iter [definition, in Coq.NArith.BinPos]
plus_iter_eq_plus [lemma, in Coq.NArith.BinPos]
plus_iter_xI [lemma, in Coq.NArith.BinPos]
plus_iter_xO [lemma, in Coq.NArith.BinPos]
plus_IZR [lemma, in Coq.Reals.RIneq]
plus_IZR_NEG_POS [lemma, in Coq.Reals.RIneq]
plus_le_compat [lemma, in Coq.Arith.Plus]
plus_le_compat_l [lemma, in Coq.Arith.Plus]
plus_le_compat_r [lemma, in Coq.Arith.Plus]
plus_le_is_le [lemma, in Coq.Reals.RIneq]
plus_le_lt_compat [lemma, in Coq.Arith.Plus]
plus_le_reg_l [lemma, in Coq.Arith.Plus]
plus_lt_compat [lemma, in Coq.Arith.Plus]
plus_lt_compat_l [lemma, in Coq.Arith.Plus]
plus_lt_compat_r [lemma, in Coq.Arith.Plus]
plus_lt_is_lt [lemma, in Coq.Reals.RIneq]
plus_lt_le_compat [lemma, in Coq.Arith.Plus]
plus_lt_reg_l [lemma, in Coq.Arith.Plus]
plus_minus [lemma, in Coq.Arith.Minus]
plus_n_O [lemma, in Coq.Init.Peano]
plus_n_Sm [lemma, in Coq.Init.Peano]
plus_O_n [lemma, in Coq.Init.Peano]
plus_permute [lemma, in Coq.Arith.Plus]
plus_permute_2_in_4 [lemma, in Coq.Arith.Plus]
plus_reg_l [lemma, in Coq.Arith.Plus]
plus_Snm_nSm [lemma, in Coq.Arith.Plus]
plus_Sn_m [lemma, in Coq.Init.Peano]
plus_sum [lemma, in Coq.Reals.PartSum]
plus_tail_plus [lemma, in Coq.Arith.Plus]
plus_0_l [lemma, in Coq.Arith.Plus]
plus_0_r [lemma, in Coq.Arith.Plus]
Pminus [definition, in Coq.NArith.BinPos]
Pminus_mask [definition, in Coq.NArith.BinPos]
Pminus_mask_carry [definition, in Coq.NArith.BinPos]
Pminus_mask_diag [lemma, in Coq.NArith.BinPos]
Pminus_mask_Gt [lemma, in Coq.NArith.BinPos]
Pmult [definition, in Coq.NArith.BinPos]
Pmult_assoc [lemma, in Coq.NArith.BinPos]
Pmult_comm [lemma, in Coq.NArith.BinPos]
Pmult_minus_distr_l [lemma, in Coq.NArith.Pnat]
Pmult_nat [definition, in Coq.NArith.BinPos]
Pmult_nat_l_plus_morphism [lemma, in Coq.NArith.Pnat]
Pmult_nat_mult_permute [lemma, in Coq.NArith.Pnat]
Pmult_nat_plus_carry_morphism [lemma, in Coq.NArith.Pnat]
Pmult_nat_r_plus_morphism [lemma, in Coq.NArith.Pnat]
Pmult_nat_succ_morphism [lemma, in Coq.NArith.Pnat]
Pmult_nat_2_mult_2_permute [lemma, in Coq.NArith.Pnat]
Pmult_nat_4_mult_2_permute [lemma, in Coq.NArith.Pnat]
Pmult_plus_distr_l [lemma, in Coq.NArith.BinPos]
Pmult_plus_distr_r [lemma, in Coq.NArith.BinPos]
Pmult_reg_l [lemma, in Coq.NArith.BinPos]
Pmult_reg_r [lemma, in Coq.NArith.BinPos]
Pmult_xI_mult_xO_discr [lemma, in Coq.NArith.BinPos]
Pmult_xI_permute_r [lemma, in Coq.NArith.BinPos]
Pmult_xO_discr [lemma, in Coq.NArith.BinPos]
Pmult_xO_permute_r [lemma, in Coq.NArith.BinPos]
Pmult_1_inversion_l [lemma, in Coq.NArith.BinPos]
Pmult_1_r [lemma, in Coq.NArith.BinPos]
Pnat [library]
PO [inductive, in Coq.Sets.Partial_Order]
point_adherent [definition, in Coq.Reals.Rtopology]
poly [lemma, in Coq.Reals.Rfunctions]
positive [inductive, in Coq.NArith.BinPos]
positive_derivative [lemma, in Coq.Reals.MVT]
positive_mask [inductive, in Coq.NArith.BinPos]
positivity_seq [definition, in Coq.Reals.AltSeries]
posreal [inductive, in Coq.Reals.RIneq]
pos_INR [lemma, in Coq.Reals.RIneq]
pos_Rl [definition, in Coq.Reals.RList]
pos_Rl_P1 [lemma, in Coq.Reals.RList]
pos_Rl_P2 [lemma, in Coq.Reals.RList]
Pow [definition, in Coq.Relations.Relation_Operators]
pow [definition, in Coq.Logic.Berardi]
pow [definition, in Coq.Reals.Rfunctions]
powerRZ [definition, in Coq.Reals.Rfunctions]
powerRZ_add [lemma, in Coq.Reals.Rfunctions]
powerRZ_le [lemma, in Coq.Reals.Rfunctions]
powerRZ_lt [lemma, in Coq.Reals.Rfunctions]
powerRZ_NOR [lemma, in Coq.Reals.Rfunctions]
powerRZ_O [lemma, in Coq.Reals.Rfunctions]
powerRZ_R1 [lemma, in Coq.Reals.Rfunctions]
powerRZ_1 [lemma, in Coq.Reals.Rfunctions]
Powerset [library]
Powerset_Classical_facts [library]
Powerset_facts [library]
Power_monotonic [lemma, in Coq.Reals.Rfunctions]
Power_set [inductive, in Coq.Sets.Powerset]
Power_set_Inhabited [lemma, in Coq.Sets.Powerset]
Power_set_PO [definition, in Coq.Sets.Powerset]
pow1 [lemma, in Coq.Reals.Rfunctions]
pow_add [lemma, in Coq.Reals.Rfunctions]
pow_fct [definition, in Coq.Reals.Ranalysis1]
pow_i [lemma, in Coq.Reals.Rtrigo_def]
pow_incr [lemma, in Coq.Reals.Rfunctions]
pow_le [lemma, in Coq.Reals.Rfunctions]
pow_lt [lemma, in Coq.Reals.Rfunctions]
pow_lt_1_zero [lemma, in Coq.Reals.Rfunctions]
pow_maj_Rabs [lemma, in Coq.Reals.Rfunctions]
pow_mult [lemma, in Coq.Reals.Rfunctions]
pow_ne_zero [lemma, in Coq.Reals.Rfunctions]
pow_nonzero [lemma, in Coq.Reals.Rfunctions]
pow_O [lemma, in Coq.Reals.Rfunctions]
pow_Rabs [lemma, in Coq.Reals.Rfunctions]
pow_RN_plus [lemma, in Coq.Reals.Rfunctions]
pow_Rsqr [lemma, in Coq.Reals.Rfunctions]
pow_R1 [lemma, in Coq.Reals.Rfunctions]
pow_R1_Rle [lemma, in Coq.Reals.Rfunctions]
pow_sqr [lemma, in Coq.Reals.Cos_rel]
Pow_x_infinity [lemma, in Coq.Reals.Rfunctions]
pow_1 [lemma, in Coq.Reals.Rfunctions]
pow_1_abs [lemma, in Coq.Reals.Rfunctions]
pow_1_even [lemma, in Coq.Reals.Rfunctions]
pow_1_odd [lemma, in Coq.Reals.Rfunctions]
pow_2_n [definition, in Coq.Reals.Rsqrt_def]
pow_2_n_growing [lemma, in Coq.Reals.Rsqrt_def]
pow_2_n_infty [lemma, in Coq.Reals.Rsqrt_def]
pow_2_n_neq_R0 [lemma, in Coq.Reals.Rsqrt_def]
Pplus [definition, in Coq.NArith.BinPos]
Pplus_assoc [lemma, in Coq.NArith.BinPos]
Pplus_carry [definition, in Coq.NArith.BinPos]
Pplus_carry_no_neutral [lemma, in Coq.NArith.BinPos]
Pplus_carry_plus [lemma, in Coq.NArith.BinPos]
Pplus_carry_pred_eq_plus [lemma, in Coq.NArith.BinPos]
Pplus_carry_reg_l [lemma, in Coq.NArith.BinPos]
Pplus_carry_reg_r [lemma, in Coq.NArith.BinPos]
Pplus_carry_spec [lemma, in Coq.NArith.BinPos]
Pplus_comm [lemma, in Coq.NArith.BinPos]
Pplus_diag [lemma, in Coq.NArith.BinPos]
Pplus_minus [lemma, in Coq.NArith.BinPos]
Pplus_no_neutral [lemma, in Coq.NArith.BinPos]
Pplus_one_succ_l [lemma, in Coq.NArith.BinPos]
Pplus_one_succ_r [lemma, in Coq.NArith.BinPos]
Pplus_reg_l [lemma, in Coq.NArith.BinPos]
Pplus_reg_r [lemma, in Coq.NArith.BinPos]
Pplus_succ_permute_l [lemma, in Coq.NArith.BinPos]
Pplus_succ_permute_r [lemma, in Coq.NArith.BinPos]
Pplus_xI_double_minus_one [lemma, in Coq.NArith.BinPos]
Pplus_xO_double_minus_one [lemma, in Coq.NArith.BinPos]
Ppred [definition, in Coq.NArith.BinPos]
Ppred_succ [lemma, in Coq.NArith.BinPos]
Prec [definition, in Coq.NArith.BinPos]
pred [definition, in Coq.Init.Peano]
PredicateExtensionality [definition, in Coq.Logic.Diaconescu]
pred_ext_and_rel_choice_imp_EM [lemma, in Coq.Logic.Diaconescu]
pred_of_minus [lemma, in Coq.Arith.Minus]
pred_o_P_of_succ_nat_o_nat_of_P_eq_id [lemma, in Coq.NArith.Pnat]
pred_Sn [lemma, in Coq.Init.Peano]
Prelude [library]
preorder [inductive, in Coq.Relations.Relation_Definitions]
Preorder [inductive, in Coq.Sets.Relations_1]
prime [inductive, in Coq.ZArith.Znumtheory]
prime_divisors [lemma, in Coq.ZArith.Znumtheory]
prime_intro [constructor, in Coq.ZArith.Znumtheory]
prime_mult [lemma, in Coq.ZArith.Znumtheory]
prime_rel_prime [lemma, in Coq.ZArith.Znumtheory]
primitive [definition, in Coq.Reals.RiemannInt]
prod [inductive, in Coq.Init.Datatypes]
prodT [inductive, in Coq.Init.Logic_Type]
prodT_curry [definition, in Coq.Init.Logic_Type]
prodT_uncurry [definition, in Coq.Init.Logic_Type]
prod_f_SO [definition, in Coq.Reals.Rprod]
prod_neq_R0 [lemma, in Coq.Reals.RIneq]
prod_SO_pos [lemma, in Coq.Reals.Rprod]
prod_SO_Rle [lemma, in Coq.Reals.Rprod]
prod_SO_split [lemma, in Coq.Reals.Rprod]
projS1 [definition, in Coq.Init.Specif]
projS2 [definition, in Coq.Init.Specif]
projT1 [definition, in Coq.Init.Specif]
projT2 [definition, in Coq.Init.Specif]
proj1 [lemma, in Coq.Init.Logic]
proj1_sig [definition, in Coq.Init.Specif]
proj2 [lemma, in Coq.Init.Logic]
proj2_sig [definition, in Coq.Init.Specif]
prolongement_C0 [lemma, in Coq.Reals.Rtopology]
ProofIrrelevance [definition, in Coq.Logic.ChoiceFacts]
ProofIrrelevance [library]
proof_irrel [lemma, in Coq.Logic.Diaconescu]
proof_irrelevance [lemma, in Coq.Logic.Classical_Prop]
proof_irrelevance [definition, in Coq.Logic.ClassicalFacts]
proof_irrelevance_cc [lemma, in Coq.Logic.ProofIrrelevance]
proof_irrelevance_cci [lemma, in Coq.Logic.ProofIrrelevance]
prop_degeneracy [definition, in Coq.Logic.ClassicalFacts]
prop_degen_em [lemma, in Coq.Logic.ClassicalFacts]
prop_degen_ext [lemma, in Coq.Logic.ClassicalFacts]
prop_eps [lemma, in Coq.Reals.Rlimit]
prop_ext [lemma, in Coq.Logic.Diaconescu]
prop_extensionality [definition, in Coq.Logic.ClassicalFacts]
prop_ext_A_eq_A_imp_A [lemma, in Coq.Logic.ClassicalFacts]
prop_ext_em_degen [lemma, in Coq.Logic.ClassicalFacts]
prop_ext_retract_A_A_imp_A [lemma, in Coq.Logic.ClassicalFacts]
Prop_S [definition, in Coq.Setoids.Setoid]
pr_nu [lemma, in Coq.Reals.Ranalysis1]
pr_nu_var [lemma, in Coq.Reals.Ranalysis4]
pr_nu_var2 [lemma, in Coq.Reals.Ranalysis4]
Pser [definition, in Coq.Reals.Rseries]
PSeries_reg [library]
Psucc [definition, in Coq.NArith.BinPos]
Psucc_discr [lemma, in Coq.NArith.BinPos]
Psucc_inj [lemma, in Coq.NArith.BinPos]
Psucc_not_one [lemma, in Coq.NArith.BinPos]
Psucc_o_double_minus_one_eq_xO [lemma, in Coq.NArith.BinPos]
Psucc_pred [lemma, in Coq.NArith.BinPos]
p2b [definition, in Coq.Logic.ProofIrrelevance]
p2p1 [lemma, in Coq.Logic.ProofIrrelevance]
p2p2 [lemma, in Coq.Logic.ProofIrrelevance]
P_nth [inductive, in Coq.Arith.Between]
P_of_succ_nat [definition, in Coq.NArith.BinPos]
P_of_succ_nat_o_nat_of_P_eq_succ [lemma, in Coq.NArith.Pnat]
P_Rmin [lemma, in Coq.Reals.Rpower]
p_xor [definition, in Coq.IntMap.Addr]
This page has been generated by coqdoc