P
P [module, in Coq.FSets.FMapAVL]
P [module, in Coq.FSets.FMapFacts]
P [module, in Coq.FSets.FSetProperties]
pair [constructor, in Coq.Init.Datatypes]
PairDecidableType [module, in Coq.Logic.DecidableTypeEx]
PairDecidableType.eq [definition, in Coq.Logic.DecidableTypeEx]
PairDecidableType.eq_dec [definition, in Coq.Logic.DecidableTypeEx]
PairDecidableType.eq_refl [lemma, in Coq.Logic.DecidableTypeEx]
PairDecidableType.eq_sym [lemma, in Coq.Logic.DecidableTypeEx]
PairDecidableType.eq_trans [lemma, in Coq.Logic.DecidableTypeEx]
PairDecidableType.t [definition, in Coq.Logic.DecidableTypeEx]
PairOrderedType [module, in Coq.FSets.OrderedTypeEx]
PairOrderedType.compare [definition, in Coq.FSets.OrderedTypeEx]
PairOrderedType.eq [definition, in Coq.FSets.OrderedTypeEx]
PairOrderedType.eq_dec [definition, in Coq.FSets.OrderedTypeEx]
PairOrderedType.eq_refl [lemma, in Coq.FSets.OrderedTypeEx]
PairOrderedType.eq_sym [lemma, in Coq.FSets.OrderedTypeEx]
PairOrderedType.eq_trans [lemma, in Coq.FSets.OrderedTypeEx]
PairOrderedType.lt [definition, in Coq.FSets.OrderedTypeEx]
PairOrderedType.lt_not_eq [lemma, in Coq.FSets.OrderedTypeEx]
PairOrderedType.lt_trans [lemma, in Coq.FSets.OrderedTypeEx]
PairOrderedType.t [definition, in Coq.FSets.OrderedTypeEx]
pairT [abbreviation, in Coq.Init.Datatypes]
PairUsualDecidableType [module, in Coq.Logic.DecidableTypeEx]
PairUsualDecidableType.eq [definition, in Coq.Logic.DecidableTypeEx]
PairUsualDecidableType.eq_dec [definition, in Coq.Logic.DecidableTypeEx]
PairUsualDecidableType.eq_refl [definition, in Coq.Logic.DecidableTypeEx]
PairUsualDecidableType.eq_sym [definition, in Coq.Logic.DecidableTypeEx]
PairUsualDecidableType.eq_trans [definition, in Coq.Logic.DecidableTypeEx]
PairUsualDecidableType.t [definition, in Coq.Logic.DecidableTypeEx]
paradox [lemma, in Coq.Logic.Hurkens]
Paradox [section, in Coq.Logic.Hurkens]
Paradox.B [variable, in Coq.Logic.Hurkens]
Paradox.bool [variable, in Coq.Logic.Hurkens]
Paradox.b2p [variable, in Coq.Logic.Hurkens]
Paradox.p2b [variable, in Coq.Logic.Hurkens]
Paradox.p2p1 [variable, in Coq.Logic.Hurkens]
Paradox.p2p2 [variable, in Coq.Logic.Hurkens]
Params [record, in Coq.Classes.Morphisms]
PartialApplication [record, in Coq.Classes.Morphisms]
PartialOrder [record, in Coq.Classes.RelationClasses]
PartialOrder [inductive, in Coq.Classes.RelationClasses]
PartialSetoid [record, in Coq.Classes.SetoidClass]
Partial_Order [library]
Partial_orders [section, in Coq.Sets.Partial_Order]
Partial_orders.p [variable, in Coq.Sets.Partial_Order]
Partial_orders.U [variable, in Coq.Sets.Partial_Order]
partial_order_antisym [instance, in Coq.Classes.RelationClasses]
partial_order_equivalence [projection, in Coq.Classes.RelationClasses]
partial_order_equivalence [constructor, in Coq.Classes.RelationClasses]
Partial_order_facts [section, in Coq.Sets.Partial_Order]
Partial_order_facts.D [variable, in Coq.Sets.Partial_Order]
Partial_order_facts.U [variable, in Coq.Sets.Partial_Order]
partition [definition, in Coq.Lists.List]
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]
Pbit [definition, in Coq.NArith.Ndigits]
Pcase [lemma, in Coq.NArith.BinPos]
Pcompare [definition, in Coq.Arith.Compare]
Pcompare [definition, in Coq.NArith.BinPos]
Pcompare_antisym [lemma, in Coq.NArith.BinPos]
Pcompare_Eq_eq [lemma, in Coq.NArith.BinPos]
Pcompare_eq_Gt [lemma, in Coq.NArith.BinPos]
Pcompare_eq_Lt [lemma, in Coq.NArith.BinPos]
Pcompare_Gt_eq_Gt [lemma, in Coq.NArith.BinPos]
Pcompare_Gt_Gt [lemma, in Coq.NArith.BinPos]
Pcompare_Gt_Lt [lemma, in Coq.NArith.BinPos]
Pcompare_Lt_eq_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_Peqb [lemma, in Coq.NArith.Ndec]
Pcompare_p_Sp [lemma, in Coq.NArith.BinPos]
Pcompare_p_Sq [lemma, in Coq.NArith.BinPos]
Pcompare_refl [lemma, in Coq.NArith.BinPos]
Pcompare_refl_id [lemma, in Coq.NArith.BinPos]
Pcompare_1 [lemma, in Coq.NArith.BinPos]
Pdiv [definition, in Coq.Numbers.Natural.BigN.Nbasic]
Pdiv2 [lemma, in Coq.ZArith.Zbinary]
Pdiv2 [definition, in Coq.NArith.BinPos]
Pdiv_eucl [definition, in Coq.ZArith.ZOdiv_def]
Pdiv_eucl_correct [lemma, in Coq.ZArith.ZOdiv_def]
Pdiv_eucl_remainder [lemma, in Coq.ZArith.ZOdiv]
Pdiv_le [lemma, in Coq.Numbers.Natural.BigN.Nbasic]
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]
PeanoOne [constructor, in Coq.NArith.BinPos]
PeanoSucc [constructor, in Coq.NArith.BinPos]
PeanoView [inductive, in Coq.NArith.BinPos]
peanoView [definition, in Coq.NArith.BinPos]
PeanoViewUnique [lemma, in Coq.NArith.BinPos]
PeanoView_iter [definition, in Coq.NArith.BinPos]
peanoView_xI [definition, in Coq.NArith.BinPos]
peanoView_xO [definition, in Coq.NArith.BinPos]
Peano_dec [library]
Peirce [lemma, in Coq.Logic.Classical_Prop]
Peqb [definition, in Coq.NArith.Ndec]
Peqb_complete [lemma, in Coq.NArith.Ndec]
Peqb_correct [lemma, in Coq.NArith.Ndec]
Peqb_Pcompare [lemma, in Coq.NArith.Ndec]
pequiv [definition, in Coq.Classes.Equivalence]
pequiv [projection, in Coq.Classes.SetoidClass]
pequiv_prf [projection, in Coq.Classes.SetoidClass]
PER [record, in Coq.Relations.Relation_Definitions]
PER [record, in Coq.Classes.RelationClasses]
PER [inductive, in Coq.Sets.Relations_1]
Perm [section, in Coq.Sorting.PermutEq]
Perm [section, in Coq.Sorting.PermutSetoid]
Permut [library]
permutation [definition, in Coq.Sorting.Permutation]
permutation [abbreviation, in Coq.Sorting.PermutEq]
Permutation [inductive, in Coq.Lists.List]
permutation [abbreviation, in Coq.Sorting.PermutSetoid]
Permutation [library]
Permutation_app [lemma, in Coq.Lists.List]
Permutation_app_head [lemma, in Coq.Lists.List]
Permutation_app_inv [lemma, in Coq.Lists.List]
Permutation_app_inv_l [lemma, in Coq.Lists.List]
Permutation_app_inv_r [lemma, in Coq.Lists.List]
Permutation_app_swap [lemma, in Coq.Lists.List]
Permutation_app_tail [lemma, in Coq.Lists.List]
Permutation_cons_app [lemma, in Coq.Lists.List]
Permutation_cons_app_inv [lemma, in Coq.Lists.List]
Permutation_cons_inv [lemma, in Coq.Lists.List]
Permutation_in [lemma, in Coq.Lists.List]
Permutation_ind_bis [lemma, in Coq.Lists.List]
Permutation_length [lemma, in Coq.Lists.List]
Permutation_map [lemma, in Coq.Lists.List]
permutation_map [lemma, in Coq.Sorting.PermutEq]
Permutation_nil [lemma, in Coq.Lists.List]
Permutation_nil_cons [lemma, in Coq.Lists.List]
permutation_Permutation [lemma, in Coq.Sorting.PermutEq]
Permutation_refl [lemma, in Coq.Lists.List]
Permutation_rev [lemma, in Coq.Lists.List]
Permutation_sym [lemma, in Coq.Lists.List]
Permutation_trans [lemma, in Coq.Lists.List]
PermutEq [library]
PermutSetoid [library]
permut_add_cons_inside [lemma, in Coq.Sorting.Permutation]
permut_add_inside [lemma, in Coq.Sorting.Permutation]
permut_app [lemma, in Coq.Sorting.Permutation]
permut_app_inv1 [lemma, in Coq.Sorting.Permutation]
permut_app_inv2 [lemma, in Coq.Sorting.Permutation]
permut_cons [lemma, in Coq.Sorting.Permutation]
permut_cons_In [lemma, in Coq.Sorting.PermutEq]
permut_cons_InA [lemma, in Coq.Sorting.PermutSetoid]
permut_conv_inv [lemma, in Coq.Sorting.Permutation]
permut_InA_InA [lemma, in Coq.Sorting.PermutSetoid]
permut_In_In [lemma, in Coq.Sorting.PermutEq]
permut_length [lemma, in Coq.Sorting.PermutSetoid]
permut_length [lemma, in Coq.Sorting.PermutEq]
permut_length_1 [lemma, in Coq.Sorting.PermutEq]
permut_length_1 [lemma, in Coq.Sorting.PermutSetoid]
permut_length_2 [lemma, in Coq.Sorting.PermutSetoid]
permut_length_2 [lemma, in Coq.Sorting.PermutEq]
permut_map [lemma, in Coq.Sorting.PermutSetoid]
permut_middle [lemma, in Coq.Sorting.Permutation]
permut_nil [lemma, in Coq.Sorting.PermutEq]
permut_nil [lemma, in Coq.Sorting.PermutSetoid]
permut_refl [lemma, in Coq.Sorting.Permutation]
permut_remove_hd [lemma, in Coq.Sorting.Permutation]
permut_rev [lemma, in Coq.Sorting.Permutation]
permut_right [abbreviation, in Coq.Sorting.Permutation]
permut_sym [lemma, in Coq.Sorting.Permutation]
permut_sym_app [lemma, in Coq.Sorting.Permutation]
permut_tran [lemma, in Coq.Sorting.Permutation]
Perm.A [variable, in Coq.Sorting.PermutEq]
Perm.A [variable, in Coq.Sorting.PermutSetoid]
Perm.B [variable, in Coq.Sorting.PermutEq]
Perm.B [variable, in Coq.Sorting.PermutSetoid]
Perm.eqA [variable, in Coq.Sorting.PermutSetoid]
Perm.eqA_dec [variable, in Coq.Sorting.PermutSetoid]
Perm.eqA_refl [variable, in Coq.Sorting.PermutSetoid]
Perm.eqA_sym [variable, in Coq.Sorting.PermutSetoid]
Perm.eqA_trans [variable, in Coq.Sorting.PermutSetoid]
Perm.eqB [variable, in Coq.Sorting.PermutSetoid]
Perm.eqB_dec [variable, in Coq.Sorting.PermutEq]
Perm.eqB_dec [variable, in Coq.Sorting.PermutSetoid]
Perm.eqB_trans [variable, in Coq.Sorting.PermutSetoid]
Perm.eq_dec [variable, in Coq.Sorting.PermutEq]
perm_left [lemma, in Coq.Sets.Permut]
perm_nil [constructor, in Coq.Lists.List]
perm_right [lemma, in Coq.Sets.Permut]
perm_skip [constructor, in Coq.Lists.List]
perm_swap [constructor, in Coq.Lists.List]
perm_trans [constructor, in Coq.Lists.List]
PER_morphism [instance, in Coq.Classes.Morphisms]
per_partial_app_morphism [instance, in Coq.Classes.Morphisms]
per_sym [projection, in Coq.Relations.Relation_Definitions]
PER_Symmetric [projection, in Coq.Classes.RelationClasses]
per_trans [projection, in Coq.Relations.Relation_Definitions]
PER_Transitive [projection, in Coq.Classes.RelationClasses]
Pgcd [definition, in Coq.ZArith.Znumtheory]
Pgcdn [definition, in Coq.ZArith.Znumtheory]
Pgcdn_correct [lemma, in Coq.ZArith.Znumtheory]
Pgcd_correct [lemma, in Coq.ZArith.Znumtheory]
Pge [definition, in Coq.NArith.BinPos]
Pggcd [definition, in Coq.ZArith.Znumtheory]
Pggcdn [definition, in Coq.ZArith.Znumtheory]
Pggcdn_correct_divisors [lemma, in Coq.ZArith.Znumtheory]
Pggcdn_gcdn [lemma, in Coq.ZArith.Znumtheory]
Pggcd_correct_divisors [lemma, in Coq.ZArith.Znumtheory]
Pggcd_gcd [lemma, in Coq.ZArith.Znumtheory]
Pgt [definition, in Coq.NArith.BinPos]
phi [definition, in Coq.Numbers.Cyclic.Int31.Int31]
Phi [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phibis_aux [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phibis_aux_bounded [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phibis_aux_equiv [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phibis_aux_lowerbound [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phibis_aux_pos [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi2 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
phi2_phi_inv2 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_bounded [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_eqn1 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_eqn2 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_gcd [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_incr [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_inv [definition, in Coq.Numbers.Cyclic.Int31.Int31]
phi_inv2 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
phi_inv_double [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_inv_double_plus_one [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_inv_incr [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_inv_phi [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_inv_phi_aux [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_inv_positive [definition, in Coq.Numbers.Cyclic.Int31.Int31]
phi_inv_positive_p2ibis [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_lowerbound [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_nz [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_phi_inv [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_phi_inv_negative [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_phi_inv_positive [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_sequence [definition, in Coq.Reals.RiemannInt]
phi_sequence_prop [lemma, in Coq.Reals.RiemannInt]
phi_twice [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_twice_firstl [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_twice_plus_one [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_twice_plus_one_firstl [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
PI [definition, in Coq.Reals.AltSeries]
PI [module, in Coq.Logic.ProofIrrelevance]
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 [definition, in Coq.NArith.BinPos]
PI.proof_irrelevance [definition, in Coq.Logic.ProofIrrelevance]
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]
Ple [definition, in Coq.NArith.BinPos]
plength [definition, in Coq.Numbers.Natural.BigN.Nbasic]
plength_correct [lemma, in Coq.Numbers.Natural.BigN.Nbasic]
plength_pred_correct [lemma, in Coq.Numbers.Natural.BigN.Nbasic]
Plt [definition, in Coq.NArith.BinPos]
Plt_ind [lemma, in Coq.NArith.BinPos]
Plt_irrefl [lemma, in Coq.NArith.BinPos]
Plt_lt_succ [lemma, in Coq.NArith.BinPos]
Plt_trans [lemma, in Coq.NArith.BinPos]
Plt_1 [lemma, in Coq.NArith.BinPos]
plus [definition, in Coq.Init.Peano]
Plus [library]
plusnS [definition, in Coq.Numbers.Natural.BigN.Nbasic]
plusn0 [definition, in Coq.Numbers.Natural.BigN.Nbasic]
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_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 [abbreviation, 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 [abbreviation, 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_succ_r_reverse [abbreviation, 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]
plus_0_r_reverse [abbreviation, in Coq.Init.Peano]
Pmax [definition, in Coq.NArith.BinPos]
Pmin [definition, in Coq.NArith.BinPos]
Pminus [definition, in Coq.NArith.BinPos]
Pminus_Eq [lemma, in Coq.NArith.BinPos]
Pminus_Lt [lemma, in Coq.NArith.BinPos]
Pminus_mask [definition, in Coq.NArith.BinPos]
Pminus_mask_carry [definition, in Coq.NArith.BinPos]
Pminus_mask_carry_diag [lemma, in Coq.NArith.BinPos]
Pminus_mask_carry_spec [lemma, in Coq.NArith.BinPos]
Pminus_mask_diag [lemma, in Coq.NArith.BinPos]
Pminus_mask_Gt [lemma, in Coq.NArith.BinPos]
Pminus_mask_IsNeg [lemma, in Coq.NArith.BinPos]
Pminus_mask_Lt [lemma, in Coq.NArith.BinPos]
Pminus_mask_succ_r [lemma, in Coq.NArith.BinPos]
Pminus_succ_r [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_Sn_m [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 [record, in Coq.Sets.Partial_Order]
pointwise_equivalence [instance, in Coq.Classes.Equivalence]
pointwise_extension [definition, in Coq.Classes.RelationClasses]
pointwise_lifting [definition, in Coq.Classes.RelationClasses]
pointwise_pointwise [lemma, in Coq.Classes.Morphisms]
pointwise_relation [definition, in Coq.Classes.Morphisms]
pointwise_subrelation [instance, in Coq.Classes.Morphisms]
point_adherent [definition, in Coq.Reals.Rtopology]
poly [lemma, in Coq.Reals.Rfunctions]
pos [projection, in Coq.Reals.RIneq]
positive [inductive, in Coq.NArith.BinPos]
PositiveMap [module, in Coq.FSets.FMapPositive]
PositiveMapAdditionalFacts [module, in Coq.FSets.FMapPositive]
PositiveMapAdditionalFacts.gsident [lemma, in Coq.FSets.FMapPositive]
PositiveMapAdditionalFacts.gsspec [lemma, in Coq.FSets.FMapPositive]
PositiveMapAdditionalFacts.map2_commut [lemma, in Coq.FSets.FMapPositive]
PositiveMapAdditionalFacts.xmap2_lr [lemma, in Coq.FSets.FMapPositive]
PositiveMap.A [section, in Coq.FSets.FMapPositive]
PositiveMap.add [definition, in Coq.FSets.FMapPositive]
PositiveMap.add_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.add_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.add_3 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.A.A [variable, in Coq.FSets.FMapPositive]
PositiveMap.A.B [variable, in Coq.FSets.FMapPositive]
PositiveMap.A.CompcertSpec [section, in Coq.FSets.FMapPositive]
PositiveMap.A.FMapSpec [section, in Coq.FSets.FMapPositive]
PositiveMap.A.FMapSpec.e [variable, in Coq.FSets.FMapPositive]
PositiveMap.A.FMapSpec.e' [variable, in Coq.FSets.FMapPositive]
PositiveMap.A.FMapSpec.m [variable, in Coq.FSets.FMapPositive]
PositiveMap.A.FMapSpec.m' [variable, in Coq.FSets.FMapPositive]
PositiveMap.A.FMapSpec.m'' [variable, in Coq.FSets.FMapPositive]
PositiveMap.A.FMapSpec.x [variable, in Coq.FSets.FMapPositive]
PositiveMap.A.FMapSpec.y [variable, in Coq.FSets.FMapPositive]
PositiveMap.A.FMapSpec.z [variable, in Coq.FSets.FMapPositive]
PositiveMap.A.Mapi [section, in Coq.FSets.FMapPositive]
PositiveMap.A.Mapi.f [variable, in Coq.FSets.FMapPositive]
PositiveMap.cardinal [definition, in Coq.FSets.FMapPositive]
PositiveMap.cardinal_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.elements [definition, in Coq.FSets.FMapPositive]
PositiveMap.elements_complete [lemma, in Coq.FSets.FMapPositive]
PositiveMap.elements_correct [lemma, in Coq.FSets.FMapPositive]
PositiveMap.elements_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.elements_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.elements_3 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.elements_3w [lemma, in Coq.FSets.FMapPositive]
PositiveMap.Empty [definition, in Coq.FSets.FMapPositive]
PositiveMap.empty [definition, in Coq.FSets.FMapPositive]
PositiveMap.Empty_alt [lemma, in Coq.FSets.FMapPositive]
PositiveMap.Empty_Node [lemma, in Coq.FSets.FMapPositive]
PositiveMap.empty_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.equal [definition, in Coq.FSets.FMapPositive]
PositiveMap.Equal [definition, in Coq.FSets.FMapPositive]
PositiveMap.equal_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.equal_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.Equiv [definition, in Coq.FSets.FMapPositive]
PositiveMap.Equivb [definition, in Coq.FSets.FMapPositive]
PositiveMap.eq_key [definition, in Coq.FSets.FMapPositive]
PositiveMap.eq_key_elt [definition, in Coq.FSets.FMapPositive]
PositiveMap.find [definition, in Coq.FSets.FMapPositive]
PositiveMap.find_xfind_h [lemma, in Coq.FSets.FMapPositive]
PositiveMap.find_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.find_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.Fold [section, in Coq.FSets.FMapPositive]
PositiveMap.fold [definition, in Coq.FSets.FMapPositive]
PositiveMap.Fold.A [variable, in Coq.FSets.FMapPositive]
PositiveMap.Fold.B [variable, in Coq.FSets.FMapPositive]
PositiveMap.Fold.f [variable, in Coq.FSets.FMapPositive]
PositiveMap.fold_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.gempty [lemma, in Coq.FSets.FMapPositive]
PositiveMap.gleaf [lemma, in Coq.FSets.FMapPositive]
PositiveMap.gmapi [lemma, in Coq.FSets.FMapPositive]
PositiveMap.gmap2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.gro [lemma, in Coq.FSets.FMapPositive]
PositiveMap.grs [lemma, in Coq.FSets.FMapPositive]
PositiveMap.gso [lemma, in Coq.FSets.FMapPositive]
PositiveMap.gss [lemma, in Coq.FSets.FMapPositive]
PositiveMap.In [definition, in Coq.FSets.FMapPositive]
PositiveMap.is_empty [definition, in Coq.FSets.FMapPositive]
PositiveMap.is_empty_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.is_empty_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.key [definition, in Coq.FSets.FMapPositive]
PositiveMap.Leaf [constructor, in Coq.FSets.FMapPositive]
PositiveMap.lt_key [definition, in Coq.FSets.FMapPositive]
PositiveMap.map [definition, in Coq.FSets.FMapPositive]
PositiveMap.mapi [definition, in Coq.FSets.FMapPositive]
PositiveMap.mapi_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.mapi_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.MapsTo [definition, in Coq.FSets.FMapPositive]
PositiveMap.MapsTo_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.map2 [definition, in Coq.FSets.FMapPositive]
PositiveMap.map2 [section, in Coq.FSets.FMapPositive]
PositiveMap.map2.A [variable, in Coq.FSets.FMapPositive]
PositiveMap.map2.B [variable, in Coq.FSets.FMapPositive]
PositiveMap.map2.C [variable, in Coq.FSets.FMapPositive]
PositiveMap.map2.f [variable, in Coq.FSets.FMapPositive]
PositiveMap.map2_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.map2_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.map_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.map_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.mem [definition, in Coq.FSets.FMapPositive]
PositiveMap.mem_find [lemma, in Coq.FSets.FMapPositive]
PositiveMap.mem_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.mem_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.Node [constructor, in Coq.FSets.FMapPositive]
PositiveMap.remove [definition, in Coq.FSets.FMapPositive]
PositiveMap.remove_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.remove_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.remove_3 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.rleaf [lemma, in Coq.FSets.FMapPositive]
PositiveMap.t [definition, in Coq.FSets.FMapPositive]
PositiveMap.tree [inductive, in Coq.FSets.FMapPositive]
PositiveMap.xelements [definition, in Coq.FSets.FMapPositive]
PositiveMap.xelements_bits_lt_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_bits_lt_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_complete [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_correct [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_hi [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_ho [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_ih [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_ii [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_io [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_oh [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_oi [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_oo [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_sort [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xfind [definition, in Coq.FSets.FMapPositive]
PositiveMap.xfind_left [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xfoldi [definition, in Coq.FSets.FMapPositive]
PositiveMap.xfoldi_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xgmapi [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xgmap2_l [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xgmap2_r [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xmapi [definition, in Coq.FSets.FMapPositive]
PositiveMap.xmap2_l [definition, in Coq.FSets.FMapPositive]
PositiveMap.xmap2_r [definition, in Coq.FSets.FMapPositive]
PositiveMap._map2 [definition, in Coq.FSets.FMapPositive]
PositiveNotOne [module, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
PositiveNotOne.not_one [axiom, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
PositiveNotOne.p [axiom, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
PositiveOrderedTypeBits [module, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.bits_lt [definition, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.bits_lt_antirefl [lemma, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.bits_lt_trans [lemma, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.compare [definition, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.eq [definition, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.eq_dec [lemma, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.eq_refl [definition, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.eq_sym [definition, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.eq_trans [definition, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.lt [definition, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.lt_not_eq [lemma, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.lt_trans [lemma, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.t [definition, in Coq.FSets.FMapPositive]
Positive_as_DT [module, in Coq.Logic.DecidableTypeEx]
Positive_as_OT [module, in Coq.FSets.OrderedTypeEx]
Positive_as_OT.compare [definition, in Coq.FSets.OrderedTypeEx]
Positive_as_OT.eq [definition, in Coq.FSets.OrderedTypeEx]
Positive_as_OT.eq_dec [definition, in Coq.FSets.OrderedTypeEx]
Positive_as_OT.eq_refl [definition, in Coq.FSets.OrderedTypeEx]
Positive_as_OT.eq_sym [definition, in Coq.FSets.OrderedTypeEx]
Positive_as_OT.eq_trans [definition, in Coq.FSets.OrderedTypeEx]
Positive_as_OT.lt [definition, in Coq.FSets.OrderedTypeEx]
Positive_as_OT.lt_not_eq [lemma, in Coq.FSets.OrderedTypeEx]
Positive_as_OT.lt_trans [lemma, in Coq.FSets.OrderedTypeEx]
Positive_as_OT.t [definition, in Coq.FSets.OrderedTypeEx]
positive_derivative [lemma, in Coq.Reals.MVT]
positive_mask [inductive, in Coq.NArith.BinPos]
positive_to_int31 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
positive_to_int31_phi_inv_positive [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
positive_to_int31_spec [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
positivity_seq [definition, in Coq.Reals.AltSeries]
posreal [record, in Coq.Reals.RIneq]
pos_INR [lemma, in Coq.Reals.RIneq]
pos_INR_nat_of_P [lemma, in Coq.Reals.RIneq]
POS_MOD [section, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
pos_mod [definition, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
POS_MOD.low [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.spec_low [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.spec_pos_mod [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.spec_to_w_Z [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.spec_to_Z [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.spec_ww_compare [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.spec_ww_digits [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.spec_ww_sub [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.spec_ww_zdigits [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.spec_w_WW [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.spec_w_0 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.spec_w_0W [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.spec_zdigits [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.w [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.ww_compare [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.ww_sub [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.ww_zdigits [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.w_compare [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.w_digits [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.w_pos_mod [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.w_to_Z [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.w_WW [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.w_zdigits [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.w_0 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
POS_MOD.w_0W [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
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.Rpow_def]
Power [abbreviation, in Coq.Wellfounded.Lexicographic_Exponentiation]
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]
Powers_of_2 [section, in Coq.ZArith.Zpower]
power_div_with_rest [section, in Coq.ZArith.Zpower]
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_IZR [lemma, in Coq.Reals.RIneq]
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]
PO_cond1 [projection, in Coq.Sets.Partial_Order]
PO_cond2 [projection, in Coq.Sets.Partial_Order]
PO_of_chain [projection, in Coq.Sets.Cpo]
PO_of_cpo [projection, in Coq.Sets.Cpo]
Pplength [definition, in Coq.NArith.Ndist]
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 [lemma, in Coq.NArith.BinPos]
Pplus_xO_double_minus_one [lemma, in Coq.NArith.BinPos]
Ppred [definition, in Coq.NArith.BinPos]
Ppred_mask [definition, in Coq.NArith.BinPos]
Ppred_minus [lemma, in Coq.NArith.BinPos]
Ppred_succ [lemma, in Coq.NArith.BinPos]
pre [projection, in Coq.Reals.RiemannInt_SF]
Prec [definition, in Coq.NArith.BinPos]
Prect [definition, in Coq.NArith.BinPos]
Prect_base [lemma, in Coq.NArith.BinPos]
Prect_succ [lemma, in Coq.NArith.BinPos]
pred [definition, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
pred [definition, in Coq.Init.Peano]
PredExt_RelChoice_imp_EM [section, in Coq.Logic.Diaconescu]
PredExt_RelChoice_imp_EM.pred_extensionality [variable, in Coq.Logic.Diaconescu]
PredExt_RelChoice_imp_EM.rel_choice [variable, in Coq.Logic.Diaconescu]
predicate [abbreviation, in Coq.Classes.RelationClasses]
predicate [definition, in Coq.Numbers.NumPrelude]
PredicateExtensionality [definition, in Coq.Logic.Diaconescu]
predicate_all [definition, in Coq.Classes.RelationClasses]
predicate_equivalence [definition, in Coq.Classes.RelationClasses]
predicate_equivalence_equivalence [instance, in Coq.Classes.RelationClasses]
predicate_equivalence_pointwise [lemma, in Coq.Classes.Morphisms_Relations]
predicate_exists [definition, in Coq.Classes.RelationClasses]
predicate_implication [definition, in Coq.Classes.RelationClasses]
predicate_implication_pointwise [lemma, in Coq.Classes.Morphisms_Relations]
predicate_implication_preorder [instance, in Coq.Classes.RelationClasses]
predicate_intersection [definition, in Coq.Classes.RelationClasses]
predicate_union [definition, in Coq.Classes.RelationClasses]
predicate_wd [definition, in Coq.Numbers.NumPrelude]
pred_c [definition, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
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]
prefix [definition, in Coq.Strings.String]
prefix_correct [lemma, in Coq.Strings.String]
Prelude [library]
Preorder [inductive, in Coq.Sets.Relations_1]
PreOrder [record, in Coq.Classes.RelationClasses]
preorder [record, in Coq.Relations.Relation_Definitions]
PreOrder_Reflexive [projection, in Coq.Classes.RelationClasses]
PreOrder_Transitive [projection, in Coq.Classes.RelationClasses]
preord_refl [projection, in Coq.Relations.Relation_Definitions]
preord_trans [projection, in Coq.Relations.Relation_Definitions]
prime [inductive, in Coq.ZArith.Znumtheory]
prime' [definition, in Coq.ZArith.Znumtheory]
prime_alt [lemma, in Coq.ZArith.Znumtheory]
prime_dec [definition, in Coq.ZArith.Znumtheory]
prime_dec_aux [definition, in Coq.ZArith.Znumtheory]
prime_divisors [lemma, in Coq.ZArith.Znumtheory]
prime_div_prime [lemma, in Coq.ZArith.Znumtheory]
prime_ge_2 [lemma, in Coq.ZArith.Znumtheory]
prime_intro [constructor, in Coq.ZArith.Znumtheory]
prime_mult [lemma, in Coq.ZArith.Znumtheory]
prime_power_prime [lemma, in Coq.ZArith.Zpow_facts]
prime_rel_prime [lemma, in Coq.ZArith.Znumtheory]
prime_2 [lemma, in Coq.ZArith.Znumtheory]
prime_3 [lemma, in Coq.ZArith.Znumtheory]
primitive [definition, in Coq.Reals.RiemannInt]
prod [inductive, in Coq.Init.Datatypes]
prodT [abbreviation, in Coq.Init.Datatypes]
prodT_curry [abbreviation, in Coq.Init.Datatypes]
prodT_ind [abbreviation, in Coq.Init.Datatypes]
prodT_rec [abbreviation, in Coq.Init.Datatypes]
prodT_rect [abbreviation, in Coq.Init.Datatypes]
prodT_uncurry [abbreviation, in Coq.Init.Datatypes]
prod_curry [definition, in Coq.Init.Datatypes]
prod_curry_uncurry [lemma, in Coq.Program.Combinators]
prod_eqdec [instance, in Coq.Classes.EquivDec]
prod_eqdec [instance, in Coq.Classes.SetoidDec]
prod_f_R0 [definition, in Coq.Reals.Rprod]
prod_f_SO [abbreviation, in Coq.Reals.Rprod]
prod_length [lemma, in Coq.Lists.List]
prod_neq_R0 [abbreviation, in Coq.Reals.RIneq]
prod_rel [definition, in Coq.Numbers.NumPrelude]
prod_rel_equiv [lemma, in Coq.Numbers.NumPrelude]
prod_rel_refl [lemma, in Coq.Numbers.NumPrelude]
prod_rel_sym [lemma, in Coq.Numbers.NumPrelude]
prod_rel_trans [lemma, in Coq.Numbers.NumPrelude]
prod_SO_pos [lemma, in Coq.Reals.Rprod]
prod_SO_Rle [lemma, in Coq.Reals.Rprod]
prod_SO_split [lemma, in Coq.Reals.Rprod]
prod_uncurry [definition, in Coq.Init.Datatypes]
prod_uncurry_curry [lemma, in Coq.Program.Combinators]
Program [library]
proj [definition, in Coq.Logic.Eqdep_dec]
Projections [section, in Coq.Init.Specif]
projections [section, in Coq.Init.Datatypes]
Projections.A [variable, in Coq.Init.Specif]
projections.A [variable, in Coq.Init.Datatypes]
projections.B [variable, in Coq.Init.Datatypes]
Projections.P [variable, in Coq.Init.Specif]
projS1 [abbreviation, in Coq.Init.Specif]
projS2 [abbreviation, in Coq.Init.Specif]
projT1 [definition, in Coq.Init.Specif]
projT1_injective [lemma, in Coq.Logic.Diaconescu]
projT2 [definition, in Coq.Init.Specif]
proj1 [lemma, in Coq.Init.Logic]
proj1_inf [definition, in Coq.Logic.ChoiceFacts]
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 [module, in Coq.Logic.ProofIrrelevanceFacts]
ProofIrrelevance [definition, in Coq.Logic.ChoiceFacts]
ProofIrrelevance [library]
ProofIrrelevanceFacts [library]
ProofIrrelevanceTheory [module, in Coq.Logic.ProofIrrelevanceFacts]
ProofIrrelevanceTheory [module, in Coq.Logic.ProofIrrelevance]
ProofIrrelevanceTheory.Eq_rect_eq.eq_rect_eq [lemma, in Coq.Logic.ProofIrrelevanceFacts]
ProofIrrelevanceTheory.subsetT_eq_compat [lemma, in Coq.Logic.ProofIrrelevanceFacts]
ProofIrrelevanceTheory.subset_eq_compat [lemma, in Coq.Logic.ProofIrrelevanceFacts]
ProofIrrelevance.proof_irrelevance [axiom, in Coq.Logic.ProofIrrelevanceFacts]
ProofIrrel_RelChoice_imp_EqEM [section, in Coq.Logic.Diaconescu]
ProofIrrel_RelChoice_imp_EqEM.A [variable, in Coq.Logic.Diaconescu]
ProofIrrel_RelChoice_imp_EqEM.a1 [variable, in Coq.Logic.Diaconescu]
ProofIrrel_RelChoice_imp_EqEM.a2 [variable, in Coq.Logic.Diaconescu]
ProofIrrel_RelChoice_imp_EqEM.proof_irrelevance [variable, in Coq.Logic.Diaconescu]
ProofIrrel_RelChoice_imp_EqEM.rel_choice [variable, in Coq.Logic.Diaconescu]
Proofs [module, in Coq.FSets.FMapAVL]
Proofs [module, in Coq.FSets.FSetAVL]
proof_irrel [lemma, in Coq.Logic.Diaconescu]
proof_irrelevance [definition, in Coq.Logic.ClassicalFacts]
proof_irrelevance [axiom, in Coq.Logic.ProofIrrelevance]
proof_irrelevance [lemma, in Coq.Logic.Classical_Prop]
proof_irrelevance_cc [lemma, in Coq.Logic.ClassicalFacts]
proof_irrelevance_cci [lemma, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_CCI [section, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_CCI.em [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_CIC [section, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC [section, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.B [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.b1 [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.b2 [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.em [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.or [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.or_dep_elim [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.or_elim [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.or_elim_redl [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.or_elim_redr [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.or_introl [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.or_intror [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_gen [section, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_gen.bool [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_gen.bool_elim [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_gen.bool_elim_redl [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_gen.bool_elim_redr [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_gen.false [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_gen.true [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_Prop_Ext_CC [section, in Coq.Logic.ClassicalFacts]
proof_irrel_rel_choice_imp_eq_dec [lemma, in Coq.Logic.Diaconescu]
proof_irrel_rel_choice_imp_eq_dec' [lemma, in Coq.Logic.Diaconescu]
Properties [module, in Coq.FSets.FSetProperties]
Properties [section, in Coq.Relations.Operators_Properties]
Properties [module, in Coq.FSets.FMapFacts]
Properties.A [variable, in Coq.Relations.Operators_Properties]
Properties.Clos_Refl_Sym_Trans [section, in Coq.Relations.Operators_Properties]
Properties.Clos_Refl_Trans [section, in Coq.Relations.Operators_Properties]
Properties.Equivalences [section, in Coq.Relations.Operators_Properties]
Properties.R [variable, in Coq.Relations.Operators_Properties]
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]
provable_prop_ext [lemma, in Coq.Logic.ClassicalFacts]
provable_prop_extensionality [definition, in Coq.Logic.ClassicalFacts]
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]
Psize [definition, in Coq.NArith.BinPos]
Psize_monotone [lemma, in Coq.NArith.BinPos]
Psquare [definition, in Coq.ZArith.Zpow_facts]
Psquare_correct [lemma, in Coq.ZArith.Zpow_facts]
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]
Ptail [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Ptail_bounded [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Ptail_pos [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
PX [module, in Coq.FSets.FMapAVL]
PX [module, in Coq.FSets.FMapWeakList]
PX [module, in Coq.FSets.FMapList]
Pxor [definition, in Coq.NArith.Ndigits]
P' [definition, in Coq.Logic.ConstructiveEpsilon]
P'_decidable [lemma, in Coq.Logic.ConstructiveEpsilon]
p2b [definition, in Coq.Logic.ClassicalFacts]
P2Bv [definition, in Coq.NArith.Ndigits]
p2i [definition, in Coq.Numbers.Cyclic.Int31.Int31]
p2ibis [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]
p2ibis_bounded [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
p2ibis_spec [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
p2i_p2ibis [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
p2p1 [lemma, in Coq.Logic.ClassicalFacts]
p2p2 [lemma, in Coq.Logic.ClassicalFacts]
P_eventually_implies_acc [lemma, in Coq.Logic.ConstructiveEpsilon]
P_eventually_implies_acc_ex [lemma, in Coq.Logic.ConstructiveEpsilon]
P_implies_acc [lemma, in Coq.Logic.ConstructiveEpsilon]
p_lt_double_digits [lemma, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDivn1]
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]