Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (21801 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (910 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (729 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1464 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (494 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (10179 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (676 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (537 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (374 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (287 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (457 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (616 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1332 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (3609 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (137 entries)

P

PackKeyedPred [constructor, in Coq.ssr.ssrbool]
PackKeyedQualifier [constructor, in Coq.ssr.ssrbool]
Padd [definition, in Coq.micromega.EnvRing]
padd [definition, in Coq.micromega.ZMicromega]
padd [definition, in Coq.micromega.RingMicromega]
Padd [definition, in Coq.setoid_ring.Ncring_polynom]
Padd [definition, in Coq.setoid_ring.Ring_polynom]
PaddC [definition, in Coq.micromega.EnvRing]
paddC [definition, in Coq.micromega.RingMicromega]
PaddC [definition, in Coq.setoid_ring.Ring_polynom]
PaddCl [definition, in Coq.setoid_ring.Ncring_polynom]
PaddCl_ok [lemma, in Coq.setoid_ring.Ncring_polynom]
PaddC_ok [lemma, in Coq.micromega.EnvRing]
PaddC_ok [definition, in Coq.micromega.RingMicromega]
PaddC_ok [lemma, in Coq.setoid_ring.Ring_polynom]
PaddI [definition, in Coq.micromega.EnvRing]
PaddI [definition, in Coq.setoid_ring.Ring_polynom]
PaddX [definition, in Coq.micromega.EnvRing]
PaddX [definition, in Coq.setoid_ring.Ncring_polynom]
PaddX [definition, in Coq.setoid_ring.Ring_polynom]
PaddXPX [lemma, in Coq.setoid_ring.Ncring_polynom]
PaddX_ok [lemma, in Coq.micromega.EnvRing]
PaddX_ok [lemma, in Coq.setoid_ring.Ncring_polynom]
PaddX_ok2 [lemma, in Coq.setoid_ring.Ncring_polynom]
PaddX_ok [lemma, in Coq.setoid_ring.Ring_polynom]
Padd_ok [lemma, in Coq.micromega.EnvRing]
Padd_ok [lemma, in Coq.setoid_ring.Ncring_polynom]
Padd_ok [lemma, in Coq.setoid_ring.Ring_polynom]
pair [constructor, in Coq.Init.Datatypes]
PairDecidableType [module, in Coq.Structures.EqualitiesFacts]
PairDecidableType [module, in Coq.Structures.DecidableTypeEx]
PairDecidableType.eq [definition, in Coq.Structures.EqualitiesFacts]
PairDecidableType.eq [definition, in Coq.Structures.DecidableTypeEx]
PairDecidableType.eq_dec [definition, in Coq.Structures.EqualitiesFacts]
PairDecidableType.eq_equiv [instance, in Coq.Structures.EqualitiesFacts]
PairDecidableType.eq_dec [definition, in Coq.Structures.DecidableTypeEx]
PairDecidableType.eq_trans [lemma, in Coq.Structures.DecidableTypeEx]
PairDecidableType.eq_sym [lemma, in Coq.Structures.DecidableTypeEx]
PairDecidableType.eq_refl [lemma, in Coq.Structures.DecidableTypeEx]
PairDecidableType.t [definition, in Coq.Structures.EqualitiesFacts]
PairDecidableType.t [definition, in Coq.Structures.DecidableTypeEx]
PairOrderedType [module, in Coq.Structures.OrdersEx]
PairOrderedType [module, in Coq.Structures.OrderedTypeEx]
PairOrderedType.compare [definition, in Coq.Structures.OrdersEx]
PairOrderedType.compare [definition, in Coq.Structures.OrderedTypeEx]
PairOrderedType.compare_spec [lemma, in Coq.Structures.OrdersEx]
PairOrderedType.eq [definition, in Coq.Structures.OrderedTypeEx]
PairOrderedType.eq_dec [definition, in Coq.Structures.OrderedTypeEx]
PairOrderedType.eq_trans [lemma, in Coq.Structures.OrderedTypeEx]
PairOrderedType.eq_sym [lemma, in Coq.Structures.OrderedTypeEx]
PairOrderedType.eq_refl [lemma, in Coq.Structures.OrderedTypeEx]
PairOrderedType.lt [definition, in Coq.Structures.OrdersEx]
PairOrderedType.lt [definition, in Coq.Structures.OrderedTypeEx]
PairOrderedType.lt_compat [instance, in Coq.Structures.OrdersEx]
PairOrderedType.lt_strorder [instance, in Coq.Structures.OrdersEx]
PairOrderedType.lt_not_eq [lemma, in Coq.Structures.OrderedTypeEx]
PairOrderedType.lt_trans [lemma, in Coq.Structures.OrderedTypeEx]
PairOrderedType.MO1 [module, in Coq.Structures.OrderedTypeEx]
PairOrderedType.MO2 [module, in Coq.Structures.OrderedTypeEx]
PairOrderedType.t [definition, in Coq.Structures.OrderedTypeEx]
pairT [abbreviation, in Coq.Init.Datatypes]
PairUsualDecidableType [module, in Coq.Structures.EqualitiesFacts]
PairUsualDecidableType [module, in Coq.Structures.DecidableTypeEx]
PairUsualDecidableType.eq [definition, in Coq.Structures.EqualitiesFacts]
PairUsualDecidableType.eq [definition, in Coq.Structures.DecidableTypeEx]
PairUsualDecidableType.eq_dec [definition, in Coq.Structures.EqualitiesFacts]
PairUsualDecidableType.eq_equiv [instance, in Coq.Structures.EqualitiesFacts]
PairUsualDecidableType.eq_dec [definition, in Coq.Structures.DecidableTypeEx]
PairUsualDecidableType.eq_trans [definition, in Coq.Structures.DecidableTypeEx]
PairUsualDecidableType.eq_sym [definition, in Coq.Structures.DecidableTypeEx]
PairUsualDecidableType.eq_refl [definition, in Coq.Structures.DecidableTypeEx]
PairUsualDecidableType.t [definition, in Coq.Structures.EqualitiesFacts]
PairUsualDecidableType.t [definition, in Coq.Structures.DecidableTypeEx]
pair_compat [instance, in Coq.Classes.RelationPairs]
pair_andP [lemma, in Coq.ssr.ssrbool]
Pand_semantics [lemma, in Coq.NArith.Ndigits]
Params [record, in Coq.Classes.Morphisms]
Params [record, in Coq.Classes.CMorphisms]
PArith [library]
PartialApplication [record, in Coq.Classes.Morphisms]
PartialApplication [record, in Coq.Classes.CMorphisms]
PartialOrder [record, in Coq.Classes.CRelationClasses]
PartialOrder [inductive, in Coq.Classes.CRelationClasses]
PartialOrder [record, in Coq.Classes.RelationClasses]
PartialOrder [inductive, in Coq.Classes.RelationClasses]
PartialOrder_StrictOrder [lemma, in Coq.Classes.Morphisms]
PartialOrder_proper [instance, in Coq.Classes.Morphisms]
PartialOrder_inverse [lemma, in Coq.Classes.CRelationClasses]
PartialOrder_inverse [lemma, in Coq.Classes.RelationClasses]
PartialOrder_StrictOrder [lemma, in Coq.Classes.CMorphisms]
PartialOrder_proper_type [instance, in Coq.Classes.CMorphisms]
PartialSetoid [record, in Coq.Classes.SetoidClass]
Partial_order_facts.D [variable, in Coq.Sets.Partial_Order]
Partial_order_facts.U [variable, in Coq.Sets.Partial_Order]
Partial_order_facts [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_orders [section, in Coq.Sets.Partial_Order]
partial_order_antisym [instance, in Coq.Classes.CRelationClasses]
partial_order_equivalence [projection, in Coq.Classes.CRelationClasses]
partial_order_equivalence [constructor, in Coq.Classes.CRelationClasses]
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 [library]
partition [definition, in Coq.Lists.List]
partition_inv_nil [lemma, in Coq.Lists.List]
partition_length [lemma, in Coq.Lists.List]
partition_cons2 [lemma, in Coq.Lists.List]
partition_cons1 [lemma, in Coq.Lists.List]
PartSum [library]
pascal [lemma, in Coq.Reals.Binomial]
pascal_step3 [lemma, in Coq.Reals.Binomial]
pascal_step2 [lemma, in Coq.Reals.Binomial]
pascal_step1 [lemma, in Coq.Reals.Binomial]
Pbit [abbreviation, in Coq.NArith.Ndigits]
Pbit_faithful [lemma, in Coq.NArith.Ndigits]
Pbit_faithful_0 [lemma, in Coq.NArith.Ndigits]
Pbit_Ptestbit [lemma, in Coq.NArith.Ndigits]
Pc [constructor, in Coq.micromega.EnvRing]
Pc [constructor, in Coq.setoid_ring.Ncring_polynom]
Pc [constructor, in Coq.setoid_ring.Ring_polynom]
pcancel [definition, in Coq.ssr.ssrfun]
pcan_pcomp [lemma, in Coq.ssr.ssrfun]
pcan_inj [lemma, in Coq.ssr.ssrfun]
Pcase [abbreviation, in Coq.PArith.BinPos]
pcomp [definition, in Coq.ssr.ssrfun]
Pcompare [definition, in Coq.Arith.Compare]
Pcompare [abbreviation, in Coq.PArith.BinPos]
Pcompare_Eq_eq [lemma, in Coq.PArith.BinPos]
Pcompare_refl [lemma, in Coq.PArith.BinPos]
Pcompare_eq_Gt [lemma, in Coq.PArith.BinPos]
Pcompare_1 [abbreviation, in Coq.PArith.BinPos]
Pcompare_succ_succ [abbreviation, in Coq.PArith.BinPos]
Pcompare_p_Sp [abbreviation, in Coq.PArith.BinPos]
Pcompare_spec [abbreviation, in Coq.PArith.BinPos]
Pcompare_antisym [abbreviation, in Coq.PArith.BinPos]
Pcompare_Lt_Gt [abbreviation, in Coq.PArith.BinPos]
Pcompare_eq_Lt [abbreviation, in Coq.PArith.BinPos]
Pcompare_Gt_Lt [abbreviation, in Coq.PArith.BinPos]
Pcompare_eq_iff [abbreviation, in Coq.PArith.BinPos]
Pcompare_refl_id [abbreviation, in Coq.PArith.BinPos]
Pcompare_Peqb [lemma, in Coq.NArith.Ndec]
Pcompare_nat_compare [abbreviation, in Coq.PArith.Pnat]
PCond [definition, in Coq.setoid_ring.Field_theory]
Pcond_simpl_complete [definition, in Coq.setoid_ring.Field_theory]
Pcond_simpl_gen [definition, in Coq.setoid_ring.Field_theory]
Pcond_Fnorm [lemma, in Coq.setoid_ring.Field_theory]
PCond_app [lemma, in Coq.setoid_ring.Field_theory]
PCond_cons_inv_r [lemma, in Coq.setoid_ring.Field_theory]
PCond_cons_inv_l [lemma, in Coq.setoid_ring.Field_theory]
PCond_cons [lemma, in Coq.setoid_ring.Field_theory]
Pdiff_semantics [lemma, in Coq.NArith.Ndigits]
Pdiv_eucl_remainder [lemma, in Coq.NArith.Ndiv_def]
Pdiv_eucl_correct [definition, in Coq.NArith.Ndiv_def]
Pdiv_eucl [definition, in Coq.NArith.Ndiv_def]
Pdiv2 [lemma, in Coq.ZArith.Zdigits]
Pdiv2 [abbreviation, in Coq.PArith.BinPos]
Pdiv2_up [abbreviation, in Coq.PArith.BinPos]
Pdouble_minus_one_o_succ_eq_xI [abbreviation, in Coq.PArith.BinPos]
Pdouble_minus_two [abbreviation, in Coq.PArith.BinPos]
Pdouble_mask [abbreviation, in Coq.PArith.BinPos]
Pdouble_plus_one_mask [abbreviation, in Coq.PArith.BinPos]
Pdouble_minus_one [abbreviation, in Coq.PArith.BinPos]
PEadd [constructor, in Coq.micromega.EnvRing]
PEadd [constructor, in Coq.setoid_ring.Ring_polynom]
PEadd_ext [instance, in Coq.setoid_ring.Field_theory]
Peano [library]
PeanoNat [library]
PeanoOne [abbreviation, in Coq.PArith.BinPos]
PeanoSucc [abbreviation, in Coq.PArith.BinPos]
peanoView [abbreviation, in Coq.PArith.BinPos]
PeanoView [abbreviation, in Coq.PArith.BinPos]
PeanoViewUnique [abbreviation, in Coq.PArith.BinPos]
PeanoView_iter [abbreviation, in Coq.PArith.BinPos]
peanoView_xI [abbreviation, in Coq.PArith.BinPos]
peanoView_xO [abbreviation, in Coq.PArith.BinPos]
PeanoView_rec [abbreviation, in Coq.PArith.BinPos]
PeanoView_ind [abbreviation, in Coq.PArith.BinPos]
PeanoView_rect [abbreviation, in Coq.PArith.BinPos]
Peano_dec [library]
PEc [constructor, in Coq.micromega.EnvRing]
PEc [constructor, in Coq.setoid_ring.Ring_polynom]
PEeval [definition, in Coq.micromega.EnvRing]
PEeval [definition, in Coq.setoid_ring.Ncring_polynom]
PEeval [definition, in Coq.setoid_ring.Ring_polynom]
PEevalR [definition, in Coq.nsatz.Nsatz]
PEI [constructor, in Coq.setoid_ring.Ring_polynom]
Peirce [lemma, in Coq.Logic.Classical_Prop]
PEmul [constructor, in Coq.micromega.EnvRing]
PEmul [constructor, in Coq.setoid_ring.Ring_polynom]
PEmul_ext [instance, in Coq.setoid_ring.Field_theory]
PEO [constructor, in Coq.setoid_ring.Ring_polynom]
PEopp [constructor, in Coq.micromega.EnvRing]
PEopp [constructor, in Coq.setoid_ring.Ring_polynom]
PEopp_ext [instance, in Coq.setoid_ring.Field_theory]
PEpow [constructor, in Coq.micromega.EnvRing]
PEpow [constructor, in Coq.setoid_ring.Ring_polynom]
PEpow_nz [lemma, in Coq.setoid_ring.Field_theory]
PEpow_mul_r [lemma, in Coq.setoid_ring.Field_theory]
PEpow_mul_l [lemma, in Coq.setoid_ring.Field_theory]
PEpow_add_r [lemma, in Coq.setoid_ring.Field_theory]
PEpow_1_l [lemma, in Coq.setoid_ring.Field_theory]
PEpow_1_r [lemma, in Coq.setoid_ring.Field_theory]
PEpow_0_r [lemma, in Coq.setoid_ring.Field_theory]
PEpow_ext [instance, in Coq.setoid_ring.Field_theory]
Peq [definition, in Coq.micromega.EnvRing]
Peq [definition, in Coq.setoid_ring.Ncring_polynom]
Peq [definition, in Coq.setoid_ring.Ring_polynom]
Peqb [abbreviation, in Coq.PArith.BinPos]
Peqb [abbreviation, in Coq.NArith.Ndec]
Peqb_true_eq [lemma, in Coq.PArith.BinPos]
Peqb_eq [abbreviation, in Coq.PArith.BinPos]
Peqb_refl [abbreviation, in Coq.PArith.BinPos]
Peqb_Pcompare [lemma, in Coq.NArith.Ndec]
Peqb_complete [lemma, in Coq.NArith.Ndec]
Peqb_correct [abbreviation, in Coq.NArith.Ndec]
pequiv [projection, in Coq.Classes.SetoidClass]
pequiv [definition, in Coq.Classes.CEquivalence]
Pequiv [definition, in Coq.setoid_ring.Ring_polynom]
pequiv [definition, in Coq.Classes.Equivalence]
pequiv_prf [projection, in Coq.Classes.SetoidClass]
Pequiv_eq [instance, in Coq.setoid_ring.Ring_polynom]
Peq_spec [lemma, in Coq.micromega.EnvRing]
Peq_ok [lemma, in Coq.micromega.EnvRing]
Peq_ok [lemma, in Coq.setoid_ring.Ncring_polynom]
Peq_spec [lemma, in Coq.setoid_ring.Ring_polynom]
Peq_ok [lemma, in Coq.setoid_ring.Ring_polynom]
PER [record, in Coq.Classes.CRelationClasses]
PER [inductive, in Coq.Sets.Relations_1]
PER [record, in Coq.Relations.Relation_Definitions]
PER [record, in Coq.Classes.RelationClasses]
Perm [section, in Coq.Sorting.PermutEq]
permA_trans [constructor, in Coq.Lists.SetoidPermutation]
permA_swap [constructor, in Coq.Lists.SetoidPermutation]
permA_skip [constructor, in Coq.Lists.SetoidPermutation]
permA_nil [constructor, in Coq.Lists.SetoidPermutation]
Permut [section, in Coq.Sorting.PermutSetoid]
Permut [library]
permutation [abbreviation, in Coq.Sorting.PermutEq]
permutation [definition, in Coq.Sorting.PermutSetoid]
Permutation [inductive, in Coq.Sorting.Permutation]
Permutation [section, in Coq.Sorting.Permutation]
Permutation [section, in Coq.Lists.SetoidPermutation]
Permutation [library]
PermutationA [inductive, in Coq.Lists.SetoidPermutation]
PermutationA_preserves_NoDupA [lemma, in Coq.Lists.SetoidPermutation]
PermutationA_decompose [lemma, in Coq.Lists.SetoidPermutation]
PermutationA_equivlistA [lemma, in Coq.Lists.SetoidPermutation]
PermutationA_middle [lemma, in Coq.Lists.SetoidPermutation]
PermutationA_cons_app [lemma, in Coq.Lists.SetoidPermutation]
PermutationA_app_comm [lemma, in Coq.Lists.SetoidPermutation]
PermutationA_cons_append [lemma, in Coq.Lists.SetoidPermutation]
PermutationA_app_tail [lemma, in Coq.Lists.SetoidPermutation]
PermutationA_app [instance, in Coq.Lists.SetoidPermutation]
PermutationA_app_head [lemma, in Coq.Lists.SetoidPermutation]
PermutationA_cons [instance, in Coq.Lists.SetoidPermutation]
permutation_map [lemma, in Coq.Sorting.PermutEq]
permutation_Permutation [lemma, in Coq.Sorting.PermutEq]
permutation_Permutation [lemma, in Coq.Sorting.PermutSetoid]
Permutation_impl_permutation [lemma, in Coq.Sorting.PermutSetoid]
Permutation_app_swap [abbreviation, in Coq.Sorting.Permutation]
Permutation_nth [lemma, in Coq.Sorting.Permutation]
Permutation_nth_error_bis [lemma, in Coq.Sorting.Permutation]
Permutation_nth_error [lemma, in Coq.Sorting.Permutation]
Permutation_alt.adapt_ok [variable, in Coq.Sorting.Permutation]
Permutation_alt.adapt_injective [variable, in Coq.Sorting.Permutation]
Permutation_alt.adapt [variable, in Coq.Sorting.Permutation]
Permutation_alt.A [variable, in Coq.Sorting.Permutation]
Permutation_alt [section, in Coq.Sorting.Permutation]
Permutation_map' [instance, in Coq.Sorting.Permutation]
Permutation_map [lemma, in Coq.Sorting.Permutation]
Permutation_map.f [variable, in Coq.Sorting.Permutation]
Permutation_map.B [variable, in Coq.Sorting.Permutation]
Permutation_map.A [variable, in Coq.Sorting.Permutation]
Permutation_map [section, in Coq.Sorting.Permutation]
Permutation_NoDup' [instance, in Coq.Sorting.Permutation]
Permutation_NoDup [lemma, in Coq.Sorting.Permutation]
Permutation_length_2 [lemma, in Coq.Sorting.Permutation]
Permutation_length_2_inv [lemma, in Coq.Sorting.Permutation]
Permutation_length_1 [lemma, in Coq.Sorting.Permutation]
Permutation_length_1_inv [lemma, in Coq.Sorting.Permutation]
Permutation_app_inv_r [lemma, in Coq.Sorting.Permutation]
Permutation_app_inv_l [lemma, in Coq.Sorting.Permutation]
Permutation_cons_app_inv [lemma, in Coq.Sorting.Permutation]
Permutation_cons_inv [lemma, in Coq.Sorting.Permutation]
Permutation_app_inv [lemma, in Coq.Sorting.Permutation]
Permutation_Add_inv [lemma, in Coq.Sorting.Permutation]
Permutation_nil_app_cons [lemma, in Coq.Sorting.Permutation]
Permutation_ind_bis [lemma, in Coq.Sorting.Permutation]
Permutation_length' [instance, in Coq.Sorting.Permutation]
Permutation_length [lemma, in Coq.Sorting.Permutation]
Permutation_rev' [instance, in Coq.Sorting.Permutation]
Permutation_rev [lemma, in Coq.Sorting.Permutation]
Permutation_middle [lemma, in Coq.Sorting.Permutation]
Permutation_Add [lemma, in Coq.Sorting.Permutation]
Permutation_cons_app [lemma, in Coq.Sorting.Permutation]
Permutation_app_comm [lemma, in Coq.Sorting.Permutation]
Permutation_cons_append [lemma, in Coq.Sorting.Permutation]
Permutation_add_inside [lemma, in Coq.Sorting.Permutation]
Permutation_app' [instance, in Coq.Sorting.Permutation]
Permutation_app [lemma, in Coq.Sorting.Permutation]
Permutation_app_head [lemma, in Coq.Sorting.Permutation]
Permutation_app_tail [lemma, in Coq.Sorting.Permutation]
Permutation_in' [instance, in Coq.Sorting.Permutation]
Permutation_in [lemma, in Coq.Sorting.Permutation]
Permutation_properties.A [variable, in Coq.Sorting.Permutation]
Permutation_properties [section, in Coq.Sorting.Permutation]
Permutation_cons [instance, in Coq.Sorting.Permutation]
Permutation_Equivalence [instance, in Coq.Sorting.Permutation]
Permutation_trans [lemma, in Coq.Sorting.Permutation]
Permutation_sym [lemma, in Coq.Sorting.Permutation]
Permutation_refl [lemma, in Coq.Sorting.Permutation]
Permutation_nil_cons [lemma, in Coq.Sorting.Permutation]
Permutation_nil [lemma, in Coq.Sorting.Permutation]
Permutation_PermutationA [lemma, in Coq.Lists.SetoidPermutation]
Permutation_eqlistA_commute [lemma, in Coq.Lists.SetoidPermutation]
Permutation.A [variable, in Coq.Sorting.Permutation]
PermutEq [library]
PermutSetoid [library]
permut_length [lemma, in Coq.Sorting.PermutEq]
permut_length_2 [lemma, in Coq.Sorting.PermutEq]
permut_length_1 [lemma, in Coq.Sorting.PermutEq]
permut_nil [lemma, in Coq.Sorting.PermutEq]
permut_cons_In [lemma, in Coq.Sorting.PermutEq]
permut_In_In [lemma, in Coq.Sorting.PermutEq]
permut_tran [abbreviation, in Coq.Sorting.PermutSetoid]
permut_right [abbreviation, in Coq.Sorting.PermutSetoid]
permut_eqA [lemma, in Coq.Sorting.PermutSetoid]
Permut_permut.eqA_equiv [variable, in Coq.Sorting.PermutSetoid]
Permut_permut.eqA_dec [variable, in Coq.Sorting.PermutSetoid]
Permut_permut.eqA [variable, in Coq.Sorting.PermutSetoid]
Permut_permut.A [variable, in Coq.Sorting.PermutSetoid]
Permut_permut [section, in Coq.Sorting.PermutSetoid]
permut_map [lemma, in Coq.Sorting.PermutSetoid]
Permut_map.eqB_trans [variable, in Coq.Sorting.PermutSetoid]
Permut_map.eqB_dec [variable, in Coq.Sorting.PermutSetoid]
Permut_map.eqB [variable, in Coq.Sorting.PermutSetoid]
Permut_map.eqA_equiv [variable, in Coq.Sorting.PermutSetoid]
Permut_map.eqA_dec [variable, in Coq.Sorting.PermutSetoid]
Permut_map.eqA [variable, in Coq.Sorting.PermutSetoid]
Permut_map.B [variable, in Coq.Sorting.PermutSetoid]
Permut_map.A [variable, in Coq.Sorting.PermutSetoid]
Permut_map [section, in Coq.Sorting.PermutSetoid]
permut_length [lemma, in Coq.Sorting.PermutSetoid]
permut_length_2 [lemma, in Coq.Sorting.PermutSetoid]
permut_length_1 [lemma, in Coq.Sorting.PermutSetoid]
permut_nil [lemma, in Coq.Sorting.PermutSetoid]
permut_cons_InA [lemma, in Coq.Sorting.PermutSetoid]
permut_InA_InA [lemma, in Coq.Sorting.PermutSetoid]
permut_remove_hd [lemma, in Coq.Sorting.PermutSetoid]
permut_remove_hd_eq [lemma, in Coq.Sorting.PermutSetoid]
permut_app_inv2 [lemma, in Coq.Sorting.PermutSetoid]
permut_app_inv1 [lemma, in Coq.Sorting.PermutSetoid]
permut_conv_inv [lemma, in Coq.Sorting.PermutSetoid]
permut_rev [lemma, in Coq.Sorting.PermutSetoid]
permut_sym_app [lemma, in Coq.Sorting.PermutSetoid]
permut_middle [lemma, in Coq.Sorting.PermutSetoid]
permut_add_cons_inside [lemma, in Coq.Sorting.PermutSetoid]
permut_add_cons_inside_eq [lemma, in Coq.Sorting.PermutSetoid]
permut_add_inside [lemma, in Coq.Sorting.PermutSetoid]
permut_add_inside_eq [lemma, in Coq.Sorting.PermutSetoid]
permut_app [lemma, in Coq.Sorting.PermutSetoid]
permut_cons [lemma, in Coq.Sorting.PermutSetoid]
permut_cons_eq [lemma, in Coq.Sorting.PermutSetoid]
permut_trans [lemma, in Coq.Sorting.PermutSetoid]
permut_sym [lemma, in Coq.Sorting.PermutSetoid]
permut_refl [lemma, in Coq.Sorting.PermutSetoid]
Permut.A [variable, in Coq.Sorting.PermutSetoid]
Permut.emptyBag [variable, in Coq.Sorting.PermutSetoid]
Permut.eqA [variable, in Coq.Sorting.PermutSetoid]
Permut.eqA_dec [variable, in Coq.Sorting.PermutSetoid]
Permut.eqA_equiv [variable, in Coq.Sorting.PermutSetoid]
Permut.singletonBag [variable, in Coq.Sorting.PermutSetoid]
perm_trans [constructor, in Coq.Sorting.Permutation]
perm_swap [constructor, in Coq.Sorting.Permutation]
perm_skip [constructor, in Coq.Sorting.Permutation]
perm_nil [constructor, in Coq.Sorting.Permutation]
perm_left [lemma, in Coq.Sets.Permut]
perm_right [lemma, in Coq.Sets.Permut]
Perm.A [variable, in Coq.Sorting.PermutEq]
Perm.B [variable, in Coq.Sorting.PermutEq]
Perm.eqB_dec [variable, in Coq.Sorting.PermutEq]
Perm.eq_dec [variable, in Coq.Sorting.PermutEq]
PER_morphism [instance, in Coq.Classes.Morphisms]
per_partial_app_morphism [instance, in Coq.Classes.Morphisms]
PER_Transitive [projection, in Coq.Classes.CRelationClasses]
PER_Symmetric [projection, in Coq.Classes.CRelationClasses]
per_trans [projection, in Coq.Relations.Relation_Definitions]
per_sym [projection, in Coq.Relations.Relation_Definitions]
PER_Transitive [projection, in Coq.Classes.RelationClasses]
PER_Symmetric [projection, in Coq.Classes.RelationClasses]
PER_type_morphism [instance, in Coq.Classes.CMorphisms]
per_partial_app_type_morphism [instance, in Coq.Classes.CMorphisms]
PEsimp [definition, in Coq.setoid_ring.Field_theory]
PEsimp_ok [lemma, in Coq.setoid_ring.Field_theory]
PEsub [constructor, in Coq.micromega.EnvRing]
PEsub [constructor, in Coq.setoid_ring.Ring_polynom]
PEsub_ext [instance, in Coq.setoid_ring.Field_theory]
PEX [constructor, in Coq.micromega.EnvRing]
PEX [constructor, in Coq.setoid_ring.Ring_polynom]
PExpr [inductive, in Coq.micromega.EnvRing]
PExpr [inductive, in Coq.setoid_ring.Ring_polynom]
PExpr_eq_spec [lemma, in Coq.setoid_ring.Field_theory]
PExpr_eq_semi_ok [lemma, in Coq.setoid_ring.Field_theory]
PExpr_eq [definition, in Coq.setoid_ring.Field_theory]
pexpr_times_nformula_correct [lemma, in Coq.micromega.RingMicromega]
pexpr_times_nformula [definition, in Coq.micromega.RingMicromega]
PEZ [definition, in Coq.nsatz.Nsatz]
PE_1_r [lemma, in Coq.setoid_ring.Field_theory]
PE_1_l [lemma, in Coq.setoid_ring.Field_theory]
PFcons_fcons_inv [lemma, in Coq.setoid_ring.Field_theory]
PFcons0_fcons_inv [lemma, in Coq.setoid_ring.Field_theory]
PFcons00_fcons_inv [lemma, in Coq.setoid_ring.Field_theory]
PFcons1_fcons_inv [lemma, in Coq.setoid_ring.Field_theory]
PFcons2_fcons_inv [lemma, in Coq.setoid_ring.Field_theory]
Pge [abbreviation, in Coq.PArith.BinPos]
Pge_ge [abbreviation, in Coq.PArith.Pnat]
Pgt [abbreviation, in Coq.PArith.BinPos]
Pgt_gt [abbreviation, in Coq.PArith.Pnat]
ph [abbreviation, in Coq.ssr.ssrbool]
ph [abbreviation, in Coq.ssr.ssrbool]
Phant [constructor, in Coq.ssr.ssreflect]
phant [inductive, in Coq.ssr.ssreflect]
Phantom [constructor, in Coq.ssr.ssreflect]
phantom [inductive, in Coq.ssr.ssreflect]
phant_id [definition, in Coq.ssr.ssrfun]
phi [definition, in Coq.Numbers.Cyclic.Int31.Int31]
phibis_aux_lowerbound [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phibis_aux_bounded [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phibis_aux_pos [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phibis_aux_equiv [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phibis_aux [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]
PhiR [definition, in Coq.nsatz.Nsatz]
phi_nz [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_gcd [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_incr [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_twice_plus_one [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_twice [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_phi_inv_positive [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_inv_positive_p2ibis [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_incr [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_inv_double [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_inv_double_plus_one [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_lowerbound [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_bounded [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_nonneg [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_twice_plus_one_firstl [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_twice_firstl [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_eqn2 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_eqn1 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
phi_sequence_prop [lemma, in Coq.Reals.RiemannInt]
phi_sequence [definition, in Coq.Reals.RiemannInt]
phi_inv2 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
phi_inv [definition, in Coq.Numbers.Cyclic.Int31.Int31]
phi_inv_positive [definition, in Coq.Numbers.Cyclic.Int31.Int31]
phi_pos1_succ [lemma, in Coq.micromega.ZCoeff]
phi_pos1_pos [lemma, in Coq.micromega.ZCoeff]
phi_pos1 [abbreviation, in Coq.micromega.ZCoeff]
phi_pos [abbreviation, in Coq.micromega.ZCoeff]
phi2 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
phi2_phi_inv2 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
PI [definition, in Coq.Reals.Rtrigo1]
PI [module, in Coq.Logic.ProofIrrelevance]
Pigeonhole [lemma, in Coq.Sets.Image]
Pigeonhole_principle [lemma, in Coq.Sets.Image]
Pigeonhole_ter [lemma, in Coq.Sets.Infinite_sets]
Pigeonhole_bis [lemma, in Coq.Sets.Infinite_sets]
Pind [abbreviation, in Coq.PArith.BinPos]
Pinj [constructor, in Coq.micromega.EnvRing]
Pinj [constructor, in Coq.setoid_ring.Ring_polynom]
Pinj_ext [instance, in Coq.setoid_ring.Ring_polynom]
Piter_op_square [lemma, in Coq.ZArith.Zpow_alt]
Piter_mul_acc [lemma, in Coq.ZArith.Zpow_alt]
Piter_op_succ [abbreviation, in Coq.PArith.BinPos]
Piter_op [abbreviation, in Coq.PArith.BinPos]
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_tg [definition, in Coq.Reals.AltSeries]
PI_neq0 [lemma, in Coq.Reals.Rtrigo1]
PI_4 [lemma, in Coq.Reals.Rtrigo1]
PI_RGT_0 [lemma, in Coq.Reals.Rtrigo1]
PI_2_aux [definition, in Coq.Reals.Rtrigo1]
PI_2_3_7_ineq [lemma, in Coq.Reals.Machin]
PI_2_3_7_tg [definition, in Coq.Reals.Machin]
PI_ineq [lemma, in Coq.Reals.Ratan]
PI.proof_irrelevance [definition, in Coq.Logic.ProofIrrelevance]
pi1 [projection, in Coq.Logic.ExtensionalityFacts]
pi2 [projection, in Coq.Logic.ExtensionalityFacts]
PI2 [definition, in Coq.Reals.Rtrigo1]
PI2_Rlt_PI [lemma, in Coq.Reals.Rtrigo1]
PI2_RGT_0 [lemma, in Coq.Reals.Rtrigo1]
pi2_int [lemma, in Coq.Reals.Rtrigo1]
PI2_1 [lemma, in Coq.Reals.Ratan]
PI2_3_2 [lemma, in Coq.Reals.Ratan]
PI2_lower_bound [lemma, in Coq.Reals.Ratan]
PI4_RGT_0 [lemma, in Coq.Reals.Rtrigo_calc]
PI4_RLT_PI2 [lemma, in Coq.Reals.Rtrigo1]
PI6_RLT_PI2 [lemma, in Coq.Reals.Rtrigo_calc]
PI6_RGT_0 [lemma, in Coq.Reals.Rtrigo_calc]
Pjump_pred_double [lemma, in Coq.micromega.EnvRing]
Pjump_xO_tail [lemma, in Coq.micromega.EnvRing]
Pjump_add [lemma, in Coq.micromega.EnvRing]
plat [definition, in Coq.Reals.Rtrigo_calc]
Ple [abbreviation, in Coq.PArith.BinPos]
Ple_succ_l [abbreviation, in Coq.PArith.BinPos]
Ple_trans [abbreviation, in Coq.PArith.BinPos]
Ple_lt_trans [abbreviation, in Coq.PArith.BinPos]
Ple_refl [abbreviation, in Coq.PArith.BinPos]
Ple_lteq [abbreviation, in Coq.PArith.BinPos]
Ple_le [abbreviation, in Coq.PArith.Pnat]
Plt [abbreviation, in Coq.PArith.BinPos]
Plt_not_plus_l [abbreviation, in Coq.PArith.BinPos]
Plt_plus_r [abbreviation, in Coq.PArith.BinPos]
Plt_succ_r [abbreviation, in Coq.PArith.BinPos]
Plt_le_trans [abbreviation, in Coq.PArith.BinPos]
Plt_ind [abbreviation, in Coq.PArith.BinPos]
Plt_trans [abbreviation, in Coq.PArith.BinPos]
Plt_irrefl [abbreviation, in Coq.PArith.BinPos]
Plt_lt_succ [abbreviation, in Coq.PArith.BinPos]
Plt_1_succ [abbreviation, in Coq.PArith.BinPos]
Plt_1 [abbreviation, in Coq.PArith.BinPos]
Plt_lt [abbreviation, in Coq.PArith.Pnat]
plus [abbreviation, in Coq.Init.Peano]
Plus [library]
plus_minus [lemma, in Coq.Arith.Minus]
plus_lt_is_lt [abbreviation, in Coq.Reals.RIneq]
plus_le_is_le [abbreviation, in Coq.Reals.RIneq]
plus_IZR [lemma, in Coq.Reals.RIneq]
plus_IZR_NEG_POS [lemma, in Coq.Reals.RIneq]
plus_INR [lemma, in Coq.Reals.RIneq]
plus_gt_compat_l [lemma, in Coq.Arith.Gt]
plus_gt_reg_l [lemma, in Coq.Arith.Gt]
plus_max_distr_r [definition, in Coq.Arith.Max]
plus_max_distr_l [definition, in Coq.Arith.Max]
plus_sum [lemma, in Coq.Reals.PartSum]
plus_fct [definition, in Coq.Reals.Ranalysis1]
plus_frac_part2 [lemma, in Coq.Reals.R_Ifp]
plus_frac_part1 [lemma, in Coq.Reals.R_Ifp]
plus_Int_part2 [lemma, in Coq.Reals.R_Ifp]
plus_Int_part1 [lemma, in Coq.Reals.R_Ifp]
plus_tail_plus [lemma, in Coq.Arith.Plus]
plus_permute_2_in_4 [abbreviation, in Coq.Arith.Plus]
plus_is_one [definition, in Coq.Arith.Plus]
plus_is_O [lemma, in Coq.Arith.Plus]
plus_lt_compat [lemma, in Coq.Arith.Plus]
plus_lt_le_compat [lemma, in Coq.Arith.Plus]
plus_le_lt_compat [lemma, in Coq.Arith.Plus]
plus_le_compat [lemma, in Coq.Arith.Plus]
plus_lt_compat_r [lemma, in Coq.Arith.Plus]
plus_lt_compat_l [lemma, in Coq.Arith.Plus]
plus_le_compat_r [lemma, in Coq.Arith.Plus]
plus_le_compat_l [lemma, in Coq.Arith.Plus]
plus_lt_reg_l [lemma, in Coq.Arith.Plus]
plus_le_reg_l [lemma, in Coq.Arith.Plus]
plus_reg_l [lemma, in Coq.Arith.Plus]
plus_assoc_reverse [lemma, in Coq.Arith.Plus]
plus_Snm_nSm [definition, in Coq.Arith.Plus]
plus_permute [abbreviation, in Coq.Arith.Plus]
plus_assoc [abbreviation, in Coq.Arith.Plus]
plus_comm [abbreviation, in Coq.Arith.Plus]
plus_0_r [abbreviation, in Coq.Arith.Plus]
plus_0_l [abbreviation, in Coq.Arith.Plus]
plus_succ_r_reverse [abbreviation, in Coq.Init.Peano]
plus_0_r_reverse [abbreviation, in Coq.Init.Peano]
plus_Sn_m [lemma, in Coq.Init.Peano]
plus_n_Sm [lemma, in Coq.Init.Peano]
plus_O_n [lemma, in Coq.Init.Peano]
plus_n_O [lemma, in Coq.Init.Peano]
plus_min_distr_r [definition, in Coq.Arith.Min]
plus_min_distr_l [definition, in Coq.Arith.Min]
plus_Rsqr_gt_0 [lemma, in Coq.Reals.Ratan]
Pmax [abbreviation, in Coq.PArith.BinPos]
Pmin [abbreviation, in Coq.PArith.BinPos]
Pminus [abbreviation, in Coq.PArith.BinPos]
Pminus_mask_Gt [lemma, in Coq.PArith.BinPos]
Pminus_Eq [abbreviation, in Coq.PArith.BinPos]
Pminus_Lt [abbreviation, in Coq.PArith.BinPos]
Pminus_mask_Lt [abbreviation, in Coq.PArith.BinPos]
Pminus_minus_distr [abbreviation, in Coq.PArith.BinPos]
Pminus_plus_distr [abbreviation, in Coq.PArith.BinPos]
Pminus_xI_xI [abbreviation, in Coq.PArith.BinPos]
Pminus_decr [abbreviation, in Coq.PArith.BinPos]
Pminus_lt_mono_r [abbreviation, in Coq.PArith.BinPos]
Pminus_compare_mono_r [abbreviation, in Coq.PArith.BinPos]
Pminus_compare_mono_l [abbreviation, in Coq.PArith.BinPos]
Pminus_lt_mono_l [abbreviation, in Coq.PArith.BinPos]
Pminus_mask_diag [abbreviation, in Coq.PArith.BinPos]
Pminus_succ_r [abbreviation, in Coq.PArith.BinPos]
Pminus_mask_carry_spec [abbreviation, in Coq.PArith.BinPos]
Pminus_mask_succ_r [abbreviation, in Coq.PArith.BinPos]
Pminus_mask_carry [abbreviation, in Coq.PArith.BinPos]
Pminus_mask [abbreviation, in Coq.PArith.BinPos]
Pminus_minus [abbreviation, in Coq.PArith.Pnat]
Pmul [definition, in Coq.micromega.EnvRing]
Pmul [definition, in Coq.setoid_ring.Ncring_polynom]
Pmul [definition, in Coq.setoid_ring.Ring_polynom]
PmulC [definition, in Coq.micromega.EnvRing]
PmulC [definition, in Coq.setoid_ring.Ncring_polynom]
PmulC [definition, in Coq.setoid_ring.Ring_polynom]
PmulC_ok [lemma, in Coq.micromega.EnvRing]
PmulC_aux_ok [lemma, in Coq.micromega.EnvRing]
PmulC_aux [definition, in Coq.micromega.EnvRing]
PmulC_ok [lemma, in Coq.setoid_ring.Ncring_polynom]
PmulC_aux_ok [lemma, in Coq.setoid_ring.Ncring_polynom]
PmulC_aux [definition, in Coq.setoid_ring.Ncring_polynom]
PmulC_ok [lemma, in Coq.setoid_ring.Ring_polynom]
PmulC_aux_ok [lemma, in Coq.setoid_ring.Ring_polynom]
PmulC_aux [definition, in Coq.setoid_ring.Ring_polynom]
PmulI [definition, in Coq.micromega.EnvRing]
PmulI [definition, in Coq.setoid_ring.Ring_polynom]
PmulI_ok [lemma, in Coq.micromega.EnvRing]
PmulI_ok [lemma, in Coq.setoid_ring.Ring_polynom]
Pmult [abbreviation, in Coq.PArith.BinPos]
Pmult_minus_distr_l [abbreviation, in Coq.PArith.BinPos]
Pmult_le_mono [abbreviation, in Coq.PArith.BinPos]
Pmult_le_mono_r [abbreviation, in Coq.PArith.BinPos]
Pmult_le_mono_l [abbreviation, in Coq.PArith.BinPos]
Pmult_lt_mono [abbreviation, in Coq.PArith.BinPos]
Pmult_lt_mono_r [abbreviation, in Coq.PArith.BinPos]
Pmult_lt_mono_l [abbreviation, in Coq.PArith.BinPos]
Pmult_compare_mono_r [abbreviation, in Coq.PArith.BinPos]
Pmult_compare_mono_l [abbreviation, in Coq.PArith.BinPos]
Pmult_1_inversion_l [abbreviation, in Coq.PArith.BinPos]
Pmult_reg_l [abbreviation, in Coq.PArith.BinPos]
Pmult_reg_r [abbreviation, in Coq.PArith.BinPos]
Pmult_xO_discr [abbreviation, in Coq.PArith.BinPos]
Pmult_xI_mult_xO_discr [abbreviation, in Coq.PArith.BinPos]
Pmult_assoc [abbreviation, in Coq.PArith.BinPos]
Pmult_plus_distr_r [abbreviation, in Coq.PArith.BinPos]
Pmult_plus_distr_l [abbreviation, in Coq.PArith.BinPos]
Pmult_comm [abbreviation, in Coq.PArith.BinPos]
Pmult_xI_permute_r [abbreviation, in Coq.PArith.BinPos]
Pmult_xO_permute_r [abbreviation, in Coq.PArith.BinPos]
Pmult_Sn_m [abbreviation, in Coq.PArith.BinPos]
Pmult_1_r [abbreviation, in Coq.PArith.BinPos]
Pmult_nat [abbreviation, in Coq.PArith.BinPos]
Pmult_nat_r_plus_morphism [lemma, in Coq.PArith.Pnat]
Pmult_nat_plus_carry_morphism [lemma, in Coq.PArith.Pnat]
Pmult_nat_l_plus_morphism [lemma, in Coq.PArith.Pnat]
Pmult_nat_succ_morphism [lemma, in Coq.PArith.Pnat]
Pmult_nat_mult [lemma, in Coq.PArith.Pnat]
Pmult_mult [abbreviation, in Coq.PArith.Pnat]
Pmul_ok [lemma, in Coq.micromega.EnvRing]
Pmul_ok [lemma, in Coq.setoid_ring.Ncring_polynom]
Pmul_ok [lemma, in Coq.setoid_ring.Ring_polynom]
Pnat [library]
PNone [constructor, in Coq.rtauto.Bintree]
PNSubst [definition, in Coq.micromega.EnvRing]
PNSubst [definition, in Coq.setoid_ring.Ring_polynom]
PNSubstL [definition, in Coq.micromega.EnvRing]
PNSubstL [definition, in Coq.setoid_ring.Ring_polynom]
PNSubstL_ok [lemma, in Coq.micromega.EnvRing]
PNSubstL_ok [lemma, in Coq.setoid_ring.Ring_polynom]
PNSubst_ok [lemma, in Coq.micromega.EnvRing]
PNSubst_ok [lemma, in Coq.setoid_ring.Ring_polynom]
PNSubst1 [definition, in Coq.micromega.EnvRing]
PNSubst1 [definition, in Coq.setoid_ring.Ring_polynom]
PNSubst1_ok [lemma, in Coq.micromega.EnvRing]
PNSubst1_ok [lemma, in Coq.setoid_ring.Ring_polynom]
PO [record, in Coq.Sets.Partial_Order]
pointwise_subrelation [instance, in Coq.Classes.Morphisms]
pointwise_pointwise [lemma, in Coq.Classes.Morphisms]
pointwise_relation [definition, in Coq.Classes.Morphisms]
pointwise_equivalence [instance, in Coq.Classes.CEquivalence]
pointwise_transitive [instance, in Coq.Classes.CEquivalence]
pointwise_symmetric [instance, in Coq.Classes.CEquivalence]
pointwise_reflexive [instance, in Coq.Classes.CEquivalence]
pointwise_lifting [definition, in Coq.Classes.RelationClasses]
pointwise_extension [definition, in Coq.Classes.RelationClasses]
pointwise_subrelation [instance, in Coq.Classes.CMorphisms]
pointwise_pointwise [lemma, in Coq.Classes.CMorphisms]
pointwise_relation [definition, in Coq.Classes.CMorphisms]
pointwise_equivalence [instance, in Coq.Classes.Equivalence]
pointwise_transitive [instance, in Coq.Classes.Equivalence]
pointwise_symmetric [instance, in Coq.Classes.Equivalence]
pointwise_reflexive [instance, in Coq.Classes.Equivalence]
point_adherent [definition, in Coq.Reals.Rtopology]
Pol [inductive, in Coq.micromega.EnvRing]
Pol [inductive, in Coq.setoid_ring.Ncring_polynom]
Pol [inductive, in Coq.setoid_ring.Ring_polynom]
PolC [definition, in Coq.micromega.RingMicromega]
PolEnv [definition, in Coq.micromega.RingMicromega]
Poly [constructor, in Coq.btauto.Algebra]
poly [inductive, in Coq.btauto.Algebra]
poly [lemma, in Coq.Reals.Rfunctions]
poly_add_linear_compat [lemma, in Coq.btauto.Algebra]
poly_mul_valid_compat [lemma, in Coq.btauto.Algebra]
poly_mul_mon_valid_compat [lemma, in Coq.btauto.Algebra]
poly_mul_mon_null_compat [lemma, in Coq.btauto.Algebra]
poly_mul_cst_valid_compat [lemma, in Coq.btauto.Algebra]
poly_add_valid_compat [lemma, in Coq.btauto.Algebra]
poly_mul_compat [lemma, in Coq.btauto.Algebra]
poly_mul_mon_compat [lemma, in Coq.btauto.Algebra]
poly_mul_cst_compat [lemma, in Coq.btauto.Algebra]
poly_add_compat [lemma, in Coq.btauto.Algebra]
poly_mul [definition, in Coq.btauto.Algebra]
poly_mul_mon [definition, in Coq.btauto.Algebra]
poly_mul_cst [definition, in Coq.btauto.Algebra]
poly_add [definition, in Coq.btauto.Algebra]
poly_of_formula_sound [lemma, in Coq.btauto.Reflect]
poly_of_formula_valid_compat [lemma, in Coq.btauto.Reflect]
poly_of_formula_eval_compat [lemma, in Coq.btauto.Reflect]
poly_of_formula [definition, in Coq.btauto.Reflect]
PolZ [definition, in Coq.nsatz.Nsatz]
PolZadd [definition, in Coq.nsatz.Nsatz]
PolZadd_correct [lemma, in Coq.nsatz.Nsatz]
PolZeq [definition, in Coq.nsatz.Nsatz]
PolZeq_correct [lemma, in Coq.nsatz.Nsatz]
PolZmul [definition, in Coq.nsatz.Nsatz]
PolZmul_correct [lemma, in Coq.nsatz.Nsatz]
POneSubst [definition, in Coq.micromega.EnvRing]
POneSubst [definition, in Coq.setoid_ring.Ring_polynom]
POneSubst_ok [lemma, in Coq.micromega.EnvRing]
POneSubst_ok [lemma, in Coq.setoid_ring.Ring_polynom]
Popp [definition, in Coq.micromega.EnvRing]
Popp [definition, in Coq.setoid_ring.Ncring_polynom]
Popp [definition, in Coq.setoid_ring.Ring_polynom]
Popp_ok [lemma, in Coq.micromega.EnvRing]
Popp_ok [lemma, in Coq.setoid_ring.Ncring_polynom]
Popp_ok [lemma, in Coq.setoid_ring.Ring_polynom]
Poption [inductive, in Coq.rtauto.Bintree]
POrderedType [library]
Por_semantics [lemma, in Coq.NArith.Ndigits]
pos [projection, in Coq.Reals.RIneq]
Pos [constructor, in Coq.Init.Decimal]
Pos [module, in Coq.PArith.BinPosDef]
Pos [module, in Coq.PArith.BinPos]
positive [abbreviation, in Coq.PArith.BinPos]
positive [inductive, in Coq.Numbers.BinNums]
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_3 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.add_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.add_1 [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.E [module, in Coq.FSets.FMapPositive]
PositiveMap.elements [definition, in Coq.FSets.FMapPositive]
PositiveMap.elements_3w [lemma, in Coq.FSets.FMapPositive]
PositiveMap.elements_3 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.elements_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.elements_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.elements_complete [lemma, in Coq.FSets.FMapPositive]
PositiveMap.elements_correct [lemma, in Coq.FSets.FMapPositive]
PositiveMap.Empty [definition, in Coq.FSets.FMapPositive]
PositiveMap.empty [definition, in Coq.FSets.FMapPositive]
PositiveMap.empty_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.Empty_Node [lemma, in Coq.FSets.FMapPositive]
PositiveMap.Empty_alt [lemma, in Coq.FSets.FMapPositive]
PositiveMap.eqke_equiv [instance, in Coq.FSets.FMapPositive]
PositiveMap.eqk_equiv [instance, in Coq.FSets.FMapPositive]
PositiveMap.Equal [definition, in Coq.FSets.FMapPositive]
PositiveMap.equal [definition, in Coq.FSets.FMapPositive]
PositiveMap.equal_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.equal_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.Equiv [definition, in Coq.FSets.FMapPositive]
PositiveMap.Equivb [definition, in Coq.FSets.FMapPositive]
PositiveMap.eq_key_elt [definition, in Coq.FSets.FMapPositive]
PositiveMap.eq_key [definition, in Coq.FSets.FMapPositive]
PositiveMap.find [definition, in Coq.FSets.FMapPositive]
PositiveMap.find_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.find_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.find_xfind_h [lemma, in Coq.FSets.FMapPositive]
PositiveMap.fold [definition, in Coq.FSets.FMapPositive]
PositiveMap.Fold [section, in Coq.FSets.FMapPositive]
PositiveMap.fold_1 [lemma, 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.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_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.is_empty_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.is_empty [definition, in Coq.FSets.FMapPositive]
PositiveMap.key [definition, in Coq.FSets.FMapPositive]
PositiveMap.Leaf [constructor, in Coq.FSets.FMapPositive]
PositiveMap.ltk_strorder [instance, 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_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.mapi_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.MapsTo [definition, in Coq.FSets.FMapPositive]
PositiveMap.MapsTo_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.map_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.map_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.map2 [definition, in Coq.FSets.FMapPositive]
PositiveMap.map2 [section, in Coq.FSets.FMapPositive]
PositiveMap.map2_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.map2_1 [lemma, 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.ME [module, in Coq.FSets.FMapPositive]
PositiveMap.mem [definition, in Coq.FSets.FMapPositive]
PositiveMap.mem_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.mem_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.mem_find [lemma, in Coq.FSets.FMapPositive]
PositiveMap.Node [constructor, in Coq.FSets.FMapPositive]
PositiveMap.remove [definition, in Coq.FSets.FMapPositive]
PositiveMap.remove_3 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.remove_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.remove_1 [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.tree_ind [definition, in Coq.FSets.FMapPositive]
PositiveMap.xelements [definition, in Coq.FSets.FMapPositive]
PositiveMap.xelements_sort [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_bits_lt_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_bits_lt_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_complete [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_ho [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_hi [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_oh [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_ih [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_oi [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_oo [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_io [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_ii [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_correct [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_r [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xgmap2_l [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xmapi [definition, in Coq.FSets.FMapPositive]
PositiveMap.xmap2_r [definition, in Coq.FSets.FMapPositive]
PositiveMap.xmap2_l [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]
PositiveOrder [module, in Coq.PArith.POrderedType]
PositiveOrderedTypeBits [module, in Coq.Structures.OrdersEx]
PositiveOrderedTypeBits [module, in Coq.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.bits_lt_trans [lemma, in Coq.Structures.OrdersEx]
PositiveOrderedTypeBits.bits_lt_antirefl [lemma, in Coq.Structures.OrdersEx]
PositiveOrderedTypeBits.bits_lt [definition, in Coq.Structures.OrdersEx]
PositiveOrderedTypeBits.bits_lt_antirefl [lemma, in Coq.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.bits_lt_trans [lemma, in Coq.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.bits_lt [definition, in Coq.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.compare [definition, in Coq.Structures.OrdersEx]
PositiveOrderedTypeBits.compare [definition, in Coq.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.compare_spec [lemma, in Coq.Structures.OrdersEx]
PositiveOrderedTypeBits.eq [definition, in Coq.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.eqb [definition, in Coq.Structures.OrdersEx]
PositiveOrderedTypeBits.eqb_eq [definition, in Coq.Structures.OrdersEx]
PositiveOrderedTypeBits.eq_dec [lemma, in Coq.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.eq_trans [definition, in Coq.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.eq_sym [definition, in Coq.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.eq_refl [definition, in Coq.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.lt [definition, in Coq.Structures.OrdersEx]
PositiveOrderedTypeBits.lt [definition, in Coq.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.lt_strorder [instance, in Coq.Structures.OrdersEx]
PositiveOrderedTypeBits.lt_compat [instance, in Coq.Structures.OrdersEx]
PositiveOrderedTypeBits.lt_not_eq [lemma, in Coq.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.lt_trans [lemma, in Coq.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.t [definition, in Coq.Structures.OrdersEx]
PositiveOrderedTypeBits.t [definition, in Coq.Structures.OrderedTypeEx]
PositiveSet [module, in Coq.FSets.FSetPositive]
PositiveSet [module, in Coq.MSets.MSetPositive]
PositiveSet.add [definition, in Coq.FSets.FSetPositive]
PositiveSet.add [definition, in Coq.MSets.MSetPositive]
PositiveSet.add_3 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.add_2 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.add_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.add_spec [lemma, in Coq.FSets.FSetPositive]
PositiveSet.add_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.cardinal [definition, in Coq.FSets.FSetPositive]
PositiveSet.cardinal [definition, in Coq.MSets.MSetPositive]
PositiveSet.cardinal_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.cardinal_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.choose [definition, in Coq.FSets.FSetPositive]
PositiveSet.choose [definition, in Coq.MSets.MSetPositive]
PositiveSet.choose_3 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.choose_3' [lemma, in Coq.FSets.FSetPositive]
PositiveSet.choose_empty [lemma, in Coq.FSets.FSetPositive]
PositiveSet.choose_2 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.choose_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.choose_spec3 [lemma, in Coq.MSets.MSetPositive]
PositiveSet.choose_spec3' [lemma, in Coq.MSets.MSetPositive]
PositiveSet.choose_empty [lemma, in Coq.MSets.MSetPositive]
PositiveSet.choose_spec2 [lemma, in Coq.MSets.MSetPositive]
PositiveSet.choose_spec1 [lemma, in Coq.MSets.MSetPositive]
PositiveSet.compare [lemma, in Coq.FSets.FSetPositive]
PositiveSet.compare [definition, in Coq.MSets.MSetPositive]
PositiveSet.compare_x_empty [lemma, in Coq.FSets.FSetPositive]
PositiveSet.compare_empty_x [lemma, in Coq.FSets.FSetPositive]
PositiveSet.compare_x_Leaf [lemma, in Coq.FSets.FSetPositive]
PositiveSet.compare_eq [lemma, in Coq.FSets.FSetPositive]
PositiveSet.compare_gt [lemma, in Coq.FSets.FSetPositive]
PositiveSet.compare_equal [lemma, in Coq.FSets.FSetPositive]
PositiveSet.compare_bool_Eq [lemma, in Coq.FSets.FSetPositive]
PositiveSet.compare_inv [lemma, in Coq.FSets.FSetPositive]
PositiveSet.compare_bool_inv [lemma, in Coq.FSets.FSetPositive]
PositiveSet.compare_fun [definition, in Coq.FSets.FSetPositive]
PositiveSet.compare_bool [definition, in Coq.FSets.FSetPositive]
PositiveSet.compare_compat [instance, in Coq.MSets.MSetPositive]
PositiveSet.compare_compat_1 [instance, in Coq.MSets.MSetPositive]
PositiveSet.compare_x_empty [lemma, in Coq.MSets.MSetPositive]
PositiveSet.compare_empty_x [lemma, in Coq.MSets.MSetPositive]
PositiveSet.compare_x_Leaf [lemma, in Coq.MSets.MSetPositive]
PositiveSet.compare_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.compare_eq [lemma, in Coq.MSets.MSetPositive]
PositiveSet.compare_gt [lemma, in Coq.MSets.MSetPositive]
PositiveSet.compare_equal [lemma, in Coq.MSets.MSetPositive]
PositiveSet.compare_bool_Eq [lemma, in Coq.MSets.MSetPositive]
PositiveSet.compare_inv [lemma, in Coq.MSets.MSetPositive]
PositiveSet.compare_bool_inv [lemma, in Coq.MSets.MSetPositive]
PositiveSet.compare_bool [definition, in Coq.MSets.MSetPositive]
PositiveSet.ct [inductive, in Coq.FSets.FSetPositive]
PositiveSet.ct [inductive, in Coq.MSets.MSetPositive]
PositiveSet.ct_compare_fun [lemma, in Coq.FSets.FSetPositive]
PositiveSet.ct_compare_bool [lemma, in Coq.FSets.FSetPositive]
PositiveSet.ct_lex [lemma, in Coq.FSets.FSetPositive]
PositiveSet.ct_xgg [lemma, in Coq.FSets.FSetPositive]
PositiveSet.ct_xll [lemma, in Coq.FSets.FSetPositive]
PositiveSet.ct_gxg [lemma, in Coq.FSets.FSetPositive]
PositiveSet.ct_lxl [lemma, in Coq.FSets.FSetPositive]
PositiveSet.ct_xce [lemma, in Coq.FSets.FSetPositive]
PositiveSet.ct_cxe [lemma, in Coq.FSets.FSetPositive]
PositiveSet.ct_lgx [constructor, in Coq.FSets.FSetPositive]
PositiveSet.ct_glx [constructor, in Coq.FSets.FSetPositive]
PositiveSet.ct_exx [constructor, in Coq.FSets.FSetPositive]
PositiveSet.ct_xex [constructor, in Coq.FSets.FSetPositive]
PositiveSet.ct_xxx [constructor, in Coq.FSets.FSetPositive]
PositiveSet.ct_compare [lemma, in Coq.MSets.MSetPositive]
PositiveSet.ct_compare_bool [lemma, in Coq.MSets.MSetPositive]
PositiveSet.ct_lex [lemma, in Coq.MSets.MSetPositive]
PositiveSet.ct_xgg [lemma, in Coq.MSets.MSetPositive]
PositiveSet.ct_xll [lemma, in Coq.MSets.MSetPositive]
PositiveSet.ct_gxg [lemma, in Coq.MSets.MSetPositive]
PositiveSet.ct_lxl [lemma, in Coq.MSets.MSetPositive]
PositiveSet.ct_xce [lemma, in Coq.MSets.MSetPositive]
PositiveSet.ct_cxe [lemma, in Coq.MSets.MSetPositive]
PositiveSet.ct_lgx [constructor, in Coq.MSets.MSetPositive]
PositiveSet.ct_glx [constructor, in Coq.MSets.MSetPositive]
PositiveSet.ct_exx [constructor, in Coq.MSets.MSetPositive]
PositiveSet.ct_xex [constructor, in Coq.MSets.MSetPositive]
PositiveSet.ct_xxx [constructor, in Coq.MSets.MSetPositive]
PositiveSet.diff [definition, in Coq.FSets.FSetPositive]
PositiveSet.diff [definition, in Coq.MSets.MSetPositive]
PositiveSet.diff_3 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.diff_2 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.diff_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.diff_spec [lemma, in Coq.FSets.FSetPositive]
PositiveSet.diff_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.E [module, in Coq.FSets.FSetPositive]
PositiveSet.E [module, in Coq.MSets.MSetPositive]
PositiveSet.elements [definition, in Coq.FSets.FSetPositive]
PositiveSet.elements [definition, in Coq.MSets.MSetPositive]
PositiveSet.elements_3w [lemma, in Coq.FSets.FSetPositive]
PositiveSet.elements_3 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.elements_2 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.elements_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.elements_spec2w [lemma, in Coq.MSets.MSetPositive]
PositiveSet.elements_spec2 [lemma, in Coq.MSets.MSetPositive]
PositiveSet.elements_spec1 [lemma, in Coq.MSets.MSetPositive]
PositiveSet.elt [definition, in Coq.FSets.FSetPositive]
PositiveSet.elt [definition, in Coq.MSets.MSetPositive]
PositiveSet.Empty [definition, in Coq.FSets.FSetPositive]
PositiveSet.empty [definition, in Coq.FSets.FSetPositive]
PositiveSet.Empty [definition, in Coq.MSets.MSetPositive]
PositiveSet.empty [definition, in Coq.MSets.MSetPositive]
PositiveSet.empty_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.empty_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.eq [definition, in Coq.FSets.FSetPositive]
PositiveSet.eq [definition, in Coq.MSets.MSetPositive]
PositiveSet.Equal [definition, in Coq.FSets.FSetPositive]
PositiveSet.equal [definition, in Coq.FSets.FSetPositive]
PositiveSet.Equal [definition, in Coq.MSets.MSetPositive]
PositiveSet.equal [definition, in Coq.MSets.MSetPositive]
PositiveSet.equal_2 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.equal_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.equal_spec [lemma, in Coq.FSets.FSetPositive]
PositiveSet.equal_subset [lemma, in Coq.FSets.FSetPositive]
PositiveSet.equal_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.equal_subset [lemma, in Coq.MSets.MSetPositive]
PositiveSet.eq_dec [lemma, in Coq.FSets.FSetPositive]
PositiveSet.eq_trans [lemma, in Coq.FSets.FSetPositive]
PositiveSet.eq_sym [lemma, in Coq.FSets.FSetPositive]
PositiveSet.eq_refl [lemma, in Coq.FSets.FSetPositive]
PositiveSet.eq_dec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.eq_equiv [instance, in Coq.MSets.MSetPositive]
PositiveSet.Exists [definition, in Coq.FSets.FSetPositive]
PositiveSet.Exists [definition, in Coq.MSets.MSetPositive]
PositiveSet.exists_2 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.exists_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.exists_ [definition, in Coq.FSets.FSetPositive]
PositiveSet.exists_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.exists_ [definition, in Coq.MSets.MSetPositive]
PositiveSet.filter [definition, in Coq.FSets.FSetPositive]
PositiveSet.filter [definition, in Coq.MSets.MSetPositive]
PositiveSet.filter_3 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.filter_2 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.filter_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.filter_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.fold [definition, in Coq.FSets.FSetPositive]
PositiveSet.Fold [section, in Coq.FSets.FSetPositive]
PositiveSet.fold [definition, in Coq.MSets.MSetPositive]
PositiveSet.Fold [section, in Coq.MSets.MSetPositive]
PositiveSet.fold_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.fold_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.Fold.B [variable, in Coq.FSets.FSetPositive]
PositiveSet.Fold.B [variable, in Coq.MSets.MSetPositive]
PositiveSet.Fold.f [variable, in Coq.FSets.FSetPositive]
PositiveSet.Fold.f [variable, in Coq.MSets.MSetPositive]
PositiveSet.for_all_2 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.for_all_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.For_all [definition, in Coq.FSets.FSetPositive]
PositiveSet.for_all [definition, in Coq.FSets.FSetPositive]
PositiveSet.for_all_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.For_all [definition, in Coq.MSets.MSetPositive]
PositiveSet.for_all [definition, in Coq.MSets.MSetPositive]
PositiveSet.In [definition, in Coq.FSets.FSetPositive]
PositiveSet.In [definition, in Coq.MSets.MSetPositive]
PositiveSet.InL [abbreviation, in Coq.FSets.FSetPositive]
PositiveSet.InL [abbreviation, in Coq.MSets.MSetPositive]
PositiveSet.inter [definition, in Coq.FSets.FSetPositive]
PositiveSet.inter [definition, in Coq.MSets.MSetPositive]
PositiveSet.inter_3 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.inter_2 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.inter_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.inter_spec [lemma, in Coq.FSets.FSetPositive]
PositiveSet.inter_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.In_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.In_compat [instance, in Coq.MSets.MSetPositive]
PositiveSet.is_empty_2 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.is_empty_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.is_empty_spec [lemma, in Coq.FSets.FSetPositive]
PositiveSet.is_empty [definition, in Coq.FSets.FSetPositive]
PositiveSet.is_empty_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.is_empty [definition, in Coq.MSets.MSetPositive]
PositiveSet.Leaf [constructor, in Coq.FSets.FSetPositive]
PositiveSet.Leaf [constructor, in Coq.MSets.MSetPositive]
PositiveSet.lex [abbreviation, in Coq.FSets.FSetPositive]
PositiveSet.lex [abbreviation, in Coq.MSets.MSetPositive]
PositiveSet.lex_Eq [lemma, in Coq.FSets.FSetPositive]
PositiveSet.lex_Opp [lemma, in Coq.FSets.FSetPositive]
PositiveSet.lex_Eq [lemma, in Coq.MSets.MSetPositive]
PositiveSet.lex_Opp [lemma, in Coq.MSets.MSetPositive]
PositiveSet.lt [definition, in Coq.FSets.FSetPositive]
PositiveSet.lt [definition, in Coq.MSets.MSetPositive]
PositiveSet.lt_rev_append [lemma, in Coq.FSets.FSetPositive]
PositiveSet.lt_not_eq [lemma, in Coq.FSets.FSetPositive]
PositiveSet.lt_trans [lemma, in Coq.FSets.FSetPositive]
PositiveSet.lt_spec [section, in Coq.FSets.FSetPositive]
PositiveSet.lt_rev_append [lemma, in Coq.MSets.MSetPositive]
PositiveSet.lt_compat [instance, in Coq.MSets.MSetPositive]
PositiveSet.lt_strorder [instance, in Coq.MSets.MSetPositive]
PositiveSet.lt_spec [section, in Coq.MSets.MSetPositive]
PositiveSet.max_elt_2 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.max_elt_3 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.max_elt_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.max_elt [definition, in Coq.FSets.FSetPositive]
PositiveSet.max_elt_spec2 [lemma, in Coq.MSets.MSetPositive]
PositiveSet.max_elt_spec3 [lemma, in Coq.MSets.MSetPositive]
PositiveSet.max_elt_spec1 [lemma, in Coq.MSets.MSetPositive]
PositiveSet.max_elt [definition, in Coq.MSets.MSetPositive]
PositiveSet.mem [definition, in Coq.FSets.FSetPositive]
PositiveSet.mem [definition, in Coq.MSets.MSetPositive]
PositiveSet.mem_node [lemma, in Coq.FSets.FSetPositive]
PositiveSet.mem_Leaf [lemma, in Coq.FSets.FSetPositive]
PositiveSet.mem_2 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.mem_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.mem_node [lemma, in Coq.MSets.MSetPositive]
PositiveSet.mem_Leaf [lemma, in Coq.MSets.MSetPositive]
PositiveSet.mem_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.min_elt_2 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.min_elt_3 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.min_elt_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.min_elt [definition, in Coq.FSets.FSetPositive]
PositiveSet.min_elt_spec2 [lemma, in Coq.MSets.MSetPositive]
PositiveSet.min_elt_spec3 [lemma, in Coq.MSets.MSetPositive]
PositiveSet.min_elt_spec1 [lemma, in Coq.MSets.MSetPositive]
PositiveSet.min_elt [definition, in Coq.MSets.MSetPositive]
PositiveSet.node [definition, in Coq.FSets.FSetPositive]
PositiveSet.Node [constructor, in Coq.FSets.FSetPositive]
PositiveSet.node [definition, in Coq.MSets.MSetPositive]
PositiveSet.Node [constructor, in Coq.MSets.MSetPositive]
PositiveSet.omap [definition, in Coq.FSets.FSetPositive]
PositiveSet.partition [definition, in Coq.FSets.FSetPositive]
PositiveSet.partition [definition, in Coq.MSets.MSetPositive]
PositiveSet.partition_2 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.partition_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.partition_filter [lemma, in Coq.FSets.FSetPositive]
PositiveSet.partition_spec2 [lemma, in Coq.MSets.MSetPositive]
PositiveSet.partition_spec1 [lemma, in Coq.MSets.MSetPositive]
PositiveSet.partition_filter [lemma, in Coq.MSets.MSetPositive]
PositiveSet.Quantifiers [section, in Coq.FSets.FSetPositive]
PositiveSet.Quantifiers [section, in Coq.MSets.MSetPositive]
PositiveSet.Quantifiers.f [variable, in Coq.FSets.FSetPositive]
PositiveSet.Quantifiers.f [variable, in Coq.MSets.MSetPositive]
PositiveSet.remove [definition, in Coq.FSets.FSetPositive]
PositiveSet.remove [definition, in Coq.MSets.MSetPositive]
PositiveSet.remove_3 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.remove_2 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.remove_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.remove_spec [lemma, in Coq.FSets.FSetPositive]
PositiveSet.remove_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.rev [definition, in Coq.FSets.FSetPositive]
PositiveSet.rev [definition, in Coq.MSets.MSetPositive]
PositiveSet.rev_append [definition, in Coq.FSets.FSetPositive]
PositiveSet.rev_append [definition, in Coq.MSets.MSetPositive]
PositiveSet.singleton [definition, in Coq.FSets.FSetPositive]
PositiveSet.singleton [definition, in Coq.MSets.MSetPositive]
PositiveSet.singleton_2 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.singleton_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.singleton_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.Subset [definition, in Coq.FSets.FSetPositive]
PositiveSet.subset [definition, in Coq.FSets.FSetPositive]
PositiveSet.Subset [definition, in Coq.MSets.MSetPositive]
PositiveSet.subset [definition, in Coq.MSets.MSetPositive]
PositiveSet.subset_2 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.subset_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.subset_spec [lemma, in Coq.FSets.FSetPositive]
PositiveSet.subset_Leaf_s [lemma, in Coq.FSets.FSetPositive]
PositiveSet.subset_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.subset_Leaf_s [lemma, in Coq.MSets.MSetPositive]
PositiveSet.t [definition, in Coq.FSets.FSetPositive]
PositiveSet.t [definition, in Coq.MSets.MSetPositive]
PositiveSet.tree [inductive, in Coq.FSets.FSetPositive]
PositiveSet.tree [inductive, in Coq.MSets.MSetPositive]
PositiveSet.tree_ind [definition, in Coq.FSets.FSetPositive]
PositiveSet.tree_ind [definition, in Coq.MSets.MSetPositive]
PositiveSet.union [definition, in Coq.FSets.FSetPositive]
PositiveSet.union [definition, in Coq.MSets.MSetPositive]
PositiveSet.union_3 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.union_2 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.union_1 [lemma, in Coq.FSets.FSetPositive]
PositiveSet.union_spec [lemma, in Coq.FSets.FSetPositive]
PositiveSet.union_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.xelements [definition, in Coq.FSets.FSetPositive]
PositiveSet.xelements [definition, in Coq.MSets.MSetPositive]
PositiveSet.xelements_spec [lemma, in Coq.FSets.FSetPositive]
PositiveSet.xelements_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.xexists [definition, in Coq.FSets.FSetPositive]
PositiveSet.xexists [definition, in Coq.MSets.MSetPositive]
PositiveSet.xexists_spec [lemma, in Coq.FSets.FSetPositive]
PositiveSet.xexists_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.xfilter [definition, in Coq.FSets.FSetPositive]
PositiveSet.xfilter [definition, in Coq.MSets.MSetPositive]
PositiveSet.xfilter_spec [lemma, in Coq.FSets.FSetPositive]
PositiveSet.xfilter_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.xfold [definition, in Coq.FSets.FSetPositive]
PositiveSet.xfold [definition, in Coq.MSets.MSetPositive]
PositiveSet.xforall [definition, in Coq.FSets.FSetPositive]
PositiveSet.xforall [definition, in Coq.MSets.MSetPositive]
PositiveSet.xforall_spec [lemma, in Coq.FSets.FSetPositive]
PositiveSet.xforall_spec [lemma, in Coq.MSets.MSetPositive]
PositiveSet.xpartition [definition, in Coq.FSets.FSetPositive]
PositiveSet.xpartition [definition, in Coq.MSets.MSetPositive]
_ [<=] _ [notation, in Coq.FSets.FSetPositive]
_ [=] _ [notation, in Coq.FSets.FSetPositive]
_ @ _ [notation, in Coq.FSets.FSetPositive]
_ [<=] _ [notation, in Coq.MSets.MSetPositive]
_ [=] _ [notation, in Coq.MSets.MSetPositive]
_ @ _ [notation, in Coq.MSets.MSetPositive]
positive_to_int31_spec [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
positive_to_int31_phi_inv_positive [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Positive_as_DT [module, in Coq.Structures.DecidableTypeEx]
positive_to_int31 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
positive_nat_N [lemma, in Coq.ZArith.Znat]
positive_N_nat [lemma, in Coq.ZArith.Znat]
positive_N_Z [lemma, in Coq.ZArith.Znat]
positive_nat_Z [lemma, in Coq.ZArith.Znat]
Positive_as_OT [module, in Coq.PArith.POrderedType]
Positive_as_DT [module, in Coq.PArith.POrderedType]
Positive_as_DT [module, in Coq.Structures.OrdersEx]
Positive_as_OT [module, in Coq.Structures.OrdersEx]
positive_eq_dec [abbreviation, in Coq.PArith.BinPos]
positive_mask_rec [abbreviation, in Coq.PArith.BinPos]
positive_mask_ind [abbreviation, in Coq.PArith.BinPos]
positive_mask_rect [abbreviation, in Coq.PArith.BinPos]
positive_mask [abbreviation, in Coq.PArith.BinPos]
positive_ind [abbreviation, in Coq.PArith.BinPos]
positive_rec [abbreviation, in Coq.PArith.BinPos]
positive_rect [abbreviation, in Coq.PArith.BinPos]
positive_derivative [lemma, in Coq.Reals.MVT]
Positive_as_OT.eq_dec [definition, in Coq.Structures.OrderedTypeEx]
Positive_as_OT.compare [definition, in Coq.Structures.OrderedTypeEx]
Positive_as_OT.lt_not_eq [lemma, in Coq.Structures.OrderedTypeEx]
Positive_as_OT.lt_trans [definition, in Coq.Structures.OrderedTypeEx]
Positive_as_OT.lt [definition, in Coq.Structures.OrderedTypeEx]
Positive_as_OT.eq_trans [definition, in Coq.Structures.OrderedTypeEx]
Positive_as_OT.eq_sym [definition, in Coq.Structures.OrderedTypeEx]
Positive_as_OT.eq_refl [definition, in Coq.Structures.OrderedTypeEx]
Positive_as_OT.eq [definition, in Coq.Structures.OrderedTypeEx]
Positive_as_OT.t [definition, in Coq.Structures.OrderedTypeEx]
Positive_as_OT [module, in Coq.Structures.OrderedTypeEx]
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_Rl_P2 [lemma, in Coq.Reals.RList]
pos_Rl_P1 [lemma, in Coq.Reals.RList]
pos_Rl [definition, in Coq.Reals.RList]
pos_mod [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
pos_bin_app [definition, in Coq.Strings.BinaryString]
pos_oct_app [definition, in Coq.Strings.OctalString]
pos_of_int [definition, in Coq.extraction.ExtrOcamlIntConv]
pos_hex_app [definition, in Coq.Strings.HexString]
pos_to_z [definition, in Coq.Numbers.AltBinNotations]
pos_of_z [definition, in Coq.Numbers.AltBinNotations]
pos_opp_lt [lemma, in Coq.Reals.Ratan]
pos_half [definition, in Coq.Reals.Ratan]
pos_half_prf [definition, in Coq.Reals.Ratan]
pos_of_bigint [definition, in Coq.extraction.ExtrOcamlBigIntConv]
pos_eq_refl [lemma, in Coq.rtauto.Rtauto]
pos_eq [definition, in Coq.rtauto.Rtauto]
Pos.add [definition, in Coq.PArith.BinPosDef]
Pos.add_carry [definition, in Coq.PArith.BinPosDef]
Pos.add_min_distr_r [lemma, in Coq.PArith.BinPos]
Pos.add_min_distr_l [lemma, in Coq.PArith.BinPos]
Pos.add_max_distr_r [lemma, in Coq.PArith.BinPos]
Pos.add_max_distr_l [lemma, in Coq.PArith.BinPos]
Pos.add_sub_assoc [lemma, in Coq.PArith.BinPos]
Pos.add_sub [lemma, in Coq.PArith.BinPos]
Pos.add_le_mono [lemma, in Coq.PArith.BinPos]
Pos.add_le_mono_r [lemma, in Coq.PArith.BinPos]
Pos.add_le_mono_l [lemma, in Coq.PArith.BinPos]
Pos.add_lt_mono [lemma, in Coq.PArith.BinPos]
Pos.add_lt_mono_r [lemma, in Coq.PArith.BinPos]
Pos.add_lt_mono_l [lemma, in Coq.PArith.BinPos]
Pos.add_compare_mono_r [lemma, in Coq.PArith.BinPos]
Pos.add_compare_mono_l [lemma, in Coq.PArith.BinPos]
Pos.add_diag [lemma, in Coq.PArith.BinPos]
Pos.add_xO_pred_double [lemma, in Coq.PArith.BinPos]
Pos.add_xI_pred_double [lemma, in Coq.PArith.BinPos]
Pos.add_xO [lemma, in Coq.PArith.BinPos]
Pos.add_assoc [lemma, in Coq.PArith.BinPos]
Pos.add_carry_reg_l [lemma, in Coq.PArith.BinPos]
Pos.add_carry_reg_r [lemma, in Coq.PArith.BinPos]
Pos.add_cancel_l [lemma, in Coq.PArith.BinPos]
Pos.add_cancel_r [lemma, in Coq.PArith.BinPos]
Pos.add_reg_l [lemma, in Coq.PArith.BinPos]
Pos.add_reg_r [lemma, in Coq.PArith.BinPos]
Pos.add_carry_add [lemma, in Coq.PArith.BinPos]
Pos.add_no_neutral [lemma, in Coq.PArith.BinPos]
Pos.add_succ_l [lemma, in Coq.PArith.BinPos]
Pos.add_succ_r [lemma, in Coq.PArith.BinPos]
Pos.add_comm [lemma, in Coq.PArith.BinPos]
Pos.add_carry_spec [lemma, in Coq.PArith.BinPos]
Pos.add_1_l [lemma, in Coq.PArith.BinPos]
Pos.add_1_r [lemma, in Coq.PArith.BinPos]
Pos.compare [definition, in Coq.PArith.BinPosDef]
Pos.compare_cont [definition, in Coq.PArith.BinPosDef]
Pos.compare_succ_succ [lemma, in Coq.PArith.BinPos]
Pos.compare_succ_l [lemma, in Coq.PArith.BinPos]
Pos.compare_succ_r [lemma, in Coq.PArith.BinPos]
Pos.compare_le_iff [lemma, in Coq.PArith.BinPos]
Pos.compare_lt_iff [lemma, in Coq.PArith.BinPos]
Pos.compare_antisym [lemma, in Coq.PArith.BinPos]
Pos.compare_eq_iff [lemma, in Coq.PArith.BinPos]
Pos.compare_cont_antisym [lemma, in Coq.PArith.BinPos]
Pos.compare_cont_refl [lemma, in Coq.PArith.BinPos]
Pos.compare_sub_mask [lemma, in Coq.PArith.BinPos]
Pos.compare_xO_xI [lemma, in Coq.PArith.BinPos]
Pos.compare_xI_xO [lemma, in Coq.PArith.BinPos]
Pos.compare_xI_xI [lemma, in Coq.PArith.BinPos]
Pos.compare_xO_xO [lemma, in Coq.PArith.BinPos]
Pos.compare_cont_Gt_not_Gt [lemma, in Coq.PArith.BinPos]
Pos.compare_cont_Gt_not_Lt [lemma, in Coq.PArith.BinPos]
Pos.compare_cont_Lt_not_Gt [lemma, in Coq.PArith.BinPos]
Pos.compare_cont_Lt_not_Lt [lemma, in Coq.PArith.BinPos]
Pos.compare_cont_Gt_Gt [lemma, in Coq.PArith.BinPos]
Pos.compare_cont_Gt_Lt [lemma, in Coq.PArith.BinPos]
Pos.compare_cont_Lt_Lt [lemma, in Coq.PArith.BinPos]
Pos.compare_cont_Lt_Gt [lemma, in Coq.PArith.BinPos]
Pos.compare_cont_Eq [lemma, in Coq.PArith.BinPos]
Pos.compare_cont_spec [lemma, in Coq.PArith.BinPos]
Pos.divide [definition, in Coq.PArith.BinPosDef]
Pos.divide_mul_r [lemma, in Coq.PArith.BinPos]
Pos.divide_mul_l [lemma, in Coq.PArith.BinPos]
Pos.divide_xO_xO [lemma, in Coq.PArith.BinPos]
Pos.divide_xO_xI [lemma, in Coq.PArith.BinPos]
Pos.divide_add_cancel_l [lemma, in Coq.PArith.BinPos]
Pos.div2 [definition, in Coq.PArith.BinPosDef]
Pos.div2_up [definition, in Coq.PArith.BinPosDef]
Pos.double_pred_mask [definition, in Coq.PArith.BinPosDef]
Pos.double_mask [definition, in Coq.PArith.BinPosDef]
Pos.double_succ [lemma, in Coq.PArith.BinPos]
Pos.eq [definition, in Coq.PArith.BinPos]
Pos.eqb [definition, in Coq.PArith.BinPosDef]
Pos.eqb_eq [lemma, in Coq.PArith.BinPos]
Pos.eq_dep_eq_positive [lemma, in Coq.PArith.BinPos]
Pos.eq_dec [lemma, in Coq.PArith.BinPos]
Pos.eq_equiv [definition, in Coq.PArith.BinPos]
Pos.gcd [definition, in Coq.PArith.BinPosDef]
Pos.gcdn [definition, in Coq.PArith.BinPosDef]
Pos.gcdn_greatest [lemma, in Coq.PArith.BinPos]
Pos.gcd_greatest [lemma, in Coq.PArith.BinPos]
Pos.gcd_divide_r [lemma, in Coq.PArith.BinPos]
Pos.gcd_divide_l [lemma, in Coq.PArith.BinPos]
Pos.ge [definition, in Coq.PArith.BinPos]
Pos.ge_le [lemma, in Coq.PArith.BinPos]
Pos.ge_le_iff [lemma, in Coq.PArith.BinPos]
Pos.ggcd [definition, in Coq.PArith.BinPosDef]
Pos.ggcdn [definition, in Coq.PArith.BinPosDef]
Pos.ggcdn_correct_divisors [lemma, in Coq.PArith.BinPos]
Pos.ggcdn_gcdn [lemma, in Coq.PArith.BinPos]
Pos.ggcd_greatest [lemma, in Coq.PArith.BinPos]
Pos.ggcd_correct_divisors [lemma, in Coq.PArith.BinPos]
Pos.ggcd_gcd [lemma, in Coq.PArith.BinPos]
Pos.gt [definition, in Coq.PArith.BinPos]
Pos.gt_lt [lemma, in Coq.PArith.BinPos]
Pos.gt_lt_iff [lemma, in Coq.PArith.BinPos]
Pos.gt_iff_add [lemma, in Coq.PArith.BinPos]
Pos.IsNeg [constructor, in Coq.PArith.BinPosDef]
Pos.IsNul [constructor, in Coq.PArith.BinPosDef]
Pos.IsPos [constructor, in Coq.PArith.BinPosDef]
Pos.iter [definition, in Coq.PArith.BinPosDef]
Pos.iter_op [definition, in Coq.PArith.BinPosDef]
Pos.iter_op_succ [lemma, in Coq.PArith.BinPos]
Pos.iter_invariant [lemma, in Coq.PArith.BinPos]
Pos.iter_add [lemma, in Coq.PArith.BinPos]
Pos.iter_succ [lemma, in Coq.PArith.BinPos]
Pos.iter_swap [lemma, in Coq.PArith.BinPos]
Pos.iter_swap_gen [lemma, in Coq.PArith.BinPos]
Pos.land [definition, in Coq.PArith.BinPosDef]
Pos.ldiff [definition, in Coq.PArith.BinPosDef]
Pos.le [definition, in Coq.PArith.BinPos]
Pos.leb [definition, in Coq.PArith.BinPosDef]
Pos.leb_le [lemma, in Coq.PArith.BinPos]
Pos.le_partorder [instance, in Coq.PArith.BinPos]
Pos.le_preorder [instance, in Coq.PArith.BinPos]
Pos.le_antisym [lemma, in Coq.PArith.BinPos]
Pos.le_succ_l [lemma, in Coq.PArith.BinPos]
Pos.le_trans [lemma, in Coq.PArith.BinPos]
Pos.le_lt_trans [lemma, in Coq.PArith.BinPos]
Pos.le_refl [lemma, in Coq.PArith.BinPos]
Pos.le_nlt [lemma, in Coq.PArith.BinPos]
Pos.le_1_l [lemma, in Coq.PArith.BinPos]
Pos.le_ge [lemma, in Coq.PArith.BinPos]
Pos.le_lteq [definition, in Coq.PArith.BinPos]
Pos.lor [definition, in Coq.PArith.BinPosDef]
Pos.lt [definition, in Coq.PArith.BinPos]
Pos.ltb [definition, in Coq.PArith.BinPosDef]
Pos.ltb_lt [lemma, in Coq.PArith.BinPos]
Pos.lt_not_add_l [lemma, in Coq.PArith.BinPos]
Pos.lt_add_r [lemma, in Coq.PArith.BinPos]
Pos.lt_add_diag_r [lemma, in Coq.PArith.BinPos]
Pos.lt_le_trans [lemma, in Coq.PArith.BinPos]
Pos.lt_total [lemma, in Coq.PArith.BinPos]
Pos.lt_compat [instance, in Coq.PArith.BinPos]
Pos.lt_strorder [instance, in Coq.PArith.BinPos]
Pos.lt_ind [lemma, in Coq.PArith.BinPos]
Pos.lt_trans [lemma, in Coq.PArith.BinPos]
Pos.lt_lt_succ [lemma, in Coq.PArith.BinPos]
Pos.lt_le_incl [lemma, in Coq.PArith.BinPos]
Pos.lt_nle [lemma, in Coq.PArith.BinPos]
Pos.lt_1_succ [lemma, in Coq.PArith.BinPos]
Pos.lt_succ_diag_r [lemma, in Coq.PArith.BinPos]
Pos.lt_succ_r [lemma, in Coq.PArith.BinPos]
Pos.lt_gt [lemma, in Coq.PArith.BinPos]
Pos.lt_iff_add [lemma, in Coq.PArith.BinPos]
Pos.lxor [definition, in Coq.PArith.BinPosDef]
Pos.mask [inductive, in Coq.PArith.BinPosDef]
Pos.mask2cmp [definition, in Coq.PArith.BinPos]
Pos.max [definition, in Coq.PArith.BinPosDef]
Pos.max_1_r [lemma, in Coq.PArith.BinPos]
Pos.max_1_l [lemma, in Coq.PArith.BinPos]
Pos.max_r [lemma, in Coq.PArith.BinPos]
Pos.max_l [lemma, in Coq.PArith.BinPos]
Pos.min [definition, in Coq.PArith.BinPosDef]
Pos.min_1_r [lemma, in Coq.PArith.BinPos]
Pos.min_1_l [lemma, in Coq.PArith.BinPos]
Pos.min_r [lemma, in Coq.PArith.BinPos]
Pos.min_l [lemma, in Coq.PArith.BinPos]
Pos.mul [definition, in Coq.PArith.BinPosDef]
Pos.mul_min_distr_r [lemma, in Coq.PArith.BinPos]
Pos.mul_min_distr_l [lemma, in Coq.PArith.BinPos]
Pos.mul_max_distr_r [lemma, in Coq.PArith.BinPos]
Pos.mul_max_distr_l [lemma, in Coq.PArith.BinPos]
Pos.mul_sub_distr_r [lemma, in Coq.PArith.BinPos]
Pos.mul_sub_distr_l [lemma, in Coq.PArith.BinPos]
Pos.mul_le_mono [lemma, in Coq.PArith.BinPos]
Pos.mul_le_mono_r [lemma, in Coq.PArith.BinPos]
Pos.mul_le_mono_l [lemma, in Coq.PArith.BinPos]
Pos.mul_lt_mono [lemma, in Coq.PArith.BinPos]
Pos.mul_lt_mono_r [lemma, in Coq.PArith.BinPos]
Pos.mul_lt_mono_l [lemma, in Coq.PArith.BinPos]
Pos.mul_compare_mono_r [lemma, in Coq.PArith.BinPos]
Pos.mul_compare_mono_l [lemma, in Coq.PArith.BinPos]
Pos.mul_eq_1 [abbreviation, in Coq.PArith.BinPos]
Pos.mul_eq_1_r [lemma, in Coq.PArith.BinPos]
Pos.mul_eq_1_l [lemma, in Coq.PArith.BinPos]
Pos.mul_cancel_l [lemma, in Coq.PArith.BinPos]
Pos.mul_cancel_r [lemma, in Coq.PArith.BinPos]
Pos.mul_reg_l [lemma, in Coq.PArith.BinPos]
Pos.mul_reg_r [lemma, in Coq.PArith.BinPos]
Pos.mul_xO_discr [lemma, in Coq.PArith.BinPos]
Pos.mul_xI_mul_xO_discr [lemma, in Coq.PArith.BinPos]
Pos.mul_succ_r [lemma, in Coq.PArith.BinPos]
Pos.mul_succ_l [lemma, in Coq.PArith.BinPos]
Pos.mul_assoc [lemma, in Coq.PArith.BinPos]
Pos.mul_add_distr_r [lemma, in Coq.PArith.BinPos]
Pos.mul_add_distr_l [lemma, in Coq.PArith.BinPos]
Pos.mul_comm [lemma, in Coq.PArith.BinPos]
Pos.mul_xI_r [lemma, in Coq.PArith.BinPos]
Pos.mul_xO_r [lemma, in Coq.PArith.BinPos]
Pos.mul_1_r [lemma, in Coq.PArith.BinPos]
Pos.mul_1_l [lemma, in Coq.PArith.BinPos]
Pos.Ndouble [definition, in Coq.PArith.BinPosDef]
Pos.nlt_1_r [lemma, in Coq.PArith.BinPos]
Pos.Nsucc_double [definition, in Coq.PArith.BinPosDef]
Pos.of_int [definition, in Coq.PArith.BinPosDef]
Pos.of_uint [definition, in Coq.PArith.BinPosDef]
Pos.of_uint_acc [definition, in Coq.PArith.BinPosDef]
Pos.of_succ_nat [definition, in Coq.PArith.BinPosDef]
Pos.of_nat [definition, in Coq.PArith.BinPosDef]
Pos.of_nat_succ [lemma, in Coq.PArith.BinPos]
Pos.PeanoOne [constructor, in Coq.PArith.BinPos]
Pos.PeanoSucc [constructor, in Coq.PArith.BinPos]
Pos.peanoView [definition, in Coq.PArith.BinPos]
Pos.PeanoView [inductive, in Coq.PArith.BinPos]
Pos.PeanoViewUnique [lemma, in Coq.PArith.BinPos]
Pos.PeanoView_iter [definition, in Coq.PArith.BinPos]
Pos.peanoView_xI [definition, in Coq.PArith.BinPos]
Pos.peanoView_xO [definition, in Coq.PArith.BinPos]
Pos.peano_equiv [lemma, in Coq.PArith.BinPos]
Pos.peano_case [lemma, in Coq.PArith.BinPos]
Pos.peano_ind [definition, in Coq.PArith.BinPos]
Pos.peano_rec [definition, in Coq.PArith.BinPos]
Pos.peano_rect_base [lemma, in Coq.PArith.BinPos]
Pos.peano_rect_succ [lemma, in Coq.PArith.BinPos]
Pos.peano_rect [definition, in Coq.PArith.BinPos]
Pos.pow [definition, in Coq.PArith.BinPosDef]
Pos.pow_gt_1 [lemma, in Coq.PArith.BinPos]
Pos.pow_succ_r [lemma, in Coq.PArith.BinPos]
Pos.pow_1_r [lemma, in Coq.PArith.BinPos]
Pos.pred [definition, in Coq.PArith.BinPosDef]
Pos.pred_mask [definition, in Coq.PArith.BinPosDef]
Pos.pred_N [definition, in Coq.PArith.BinPosDef]
Pos.pred_double [definition, in Coq.PArith.BinPosDef]
Pos.pred_of_succ_nat [lemma, in Coq.PArith.BinPos]
Pos.pred_sub [lemma, in Coq.PArith.BinPos]
Pos.pred_N_succ [lemma, in Coq.PArith.BinPos]
Pos.pred_succ [lemma, in Coq.PArith.BinPos]
Pos.pred_double_xO_discr [lemma, in Coq.PArith.BinPos]
Pos.pred_double_succ [lemma, in Coq.PArith.BinPos]
Pos.pred_double_spec [lemma, in Coq.PArith.BinPos]
Pos.shiftl [definition, in Coq.PArith.BinPosDef]
Pos.shiftl_nat [definition, in Coq.PArith.BinPosDef]
Pos.shiftr [definition, in Coq.PArith.BinPosDef]
Pos.shiftr_nat [definition, in Coq.PArith.BinPosDef]
Pos.size [definition, in Coq.PArith.BinPosDef]
Pos.size_nat [definition, in Coq.PArith.BinPosDef]
Pos.size_le [lemma, in Coq.PArith.BinPos]
Pos.size_gt [lemma, in Coq.PArith.BinPos]
Pos.size_nat_monotone [lemma, in Coq.PArith.BinPos]
Pos.sqrt [definition, in Coq.PArith.BinPosDef]
Pos.SqrtApprox [constructor, in Coq.PArith.BinPos]
Pos.SqrtExact [constructor, in Coq.PArith.BinPos]
Pos.sqrtrem [definition, in Coq.PArith.BinPosDef]
Pos.sqrtrem_step [definition, in Coq.PArith.BinPosDef]
Pos.sqrtrem_spec [lemma, in Coq.PArith.BinPos]
Pos.sqrtrem_step_spec [lemma, in Coq.PArith.BinPos]
Pos.SqrtSpec [inductive, in Coq.PArith.BinPos]
Pos.sqrt_spec [lemma, in Coq.PArith.BinPos]
Pos.square [definition, in Coq.PArith.BinPosDef]
Pos.square_spec [lemma, in Coq.PArith.BinPos]
Pos.square_xI [lemma, in Coq.PArith.BinPos]
Pos.square_xO [lemma, in Coq.PArith.BinPos]
Pos.sub [definition, in Coq.PArith.BinPosDef]
Pos.SubIsNeg [constructor, in Coq.PArith.BinPos]
Pos.SubIsNul [constructor, in Coq.PArith.BinPos]
Pos.SubIsPos [constructor, in Coq.PArith.BinPos]
Pos.SubMaskSpec [inductive, in Coq.PArith.BinPos]
Pos.sub_mask_carry [definition, in Coq.PArith.BinPosDef]
Pos.sub_mask [definition, in Coq.PArith.BinPosDef]
Pos.sub_diag [lemma, in Coq.PArith.BinPos]
Pos.sub_lt [lemma, in Coq.PArith.BinPos]
Pos.sub_le [lemma, in Coq.PArith.BinPos]
Pos.sub_mask_neg [lemma, in Coq.PArith.BinPos]
Pos.sub_mask_neg_iff' [lemma, in Coq.PArith.BinPos]
Pos.sub_xO_xI [lemma, in Coq.PArith.BinPos]
Pos.sub_xI_xO [lemma, in Coq.PArith.BinPos]
Pos.sub_xI_xI [lemma, in Coq.PArith.BinPos]
Pos.sub_xO_xO [lemma, in Coq.PArith.BinPos]
Pos.sub_sub_distr [lemma, in Coq.PArith.BinPos]
Pos.sub_add_distr [lemma, in Coq.PArith.BinPos]
Pos.sub_decr [lemma, in Coq.PArith.BinPos]
Pos.sub_lt_mono_r [lemma, in Coq.PArith.BinPos]
Pos.sub_compare_mono_r [lemma, in Coq.PArith.BinPos]
Pos.sub_compare_mono_l [lemma, in Coq.PArith.BinPos]
Pos.sub_lt_mono_l [lemma, in Coq.PArith.BinPos]
Pos.sub_add [lemma, in Coq.PArith.BinPos]
Pos.sub_mask_pos [lemma, in Coq.PArith.BinPos]
Pos.sub_mask_pos' [lemma, in Coq.PArith.BinPos]
Pos.sub_succ_r [lemma, in Coq.PArith.BinPos]
Pos.sub_1_r [lemma, in Coq.PArith.BinPos]
Pos.sub_mask_neg_iff [lemma, in Coq.PArith.BinPos]
Pos.sub_mask_add_diag_r [lemma, in Coq.PArith.BinPos]
Pos.sub_mask_pos_iff [lemma, in Coq.PArith.BinPos]
Pos.sub_mask_add_diag_l [lemma, in Coq.PArith.BinPos]
Pos.sub_mask_add [lemma, in Coq.PArith.BinPos]
Pos.sub_mask_diag [lemma, in Coq.PArith.BinPos]
Pos.sub_mask_nul_iff [lemma, in Coq.PArith.BinPos]
Pos.sub_mask_spec [lemma, in Coq.PArith.BinPos]
Pos.sub_mask_carry_spec [lemma, in Coq.PArith.BinPos]
Pos.sub_mask_succ_r [lemma, in Coq.PArith.BinPos]
Pos.succ [definition, in Coq.PArith.BinPosDef]
Pos.succ_double_mask [definition, in Coq.PArith.BinPosDef]
Pos.succ_of_nat [lemma, in Coq.PArith.BinPos]
Pos.succ_min_distr [lemma, in Coq.PArith.BinPos]
Pos.succ_max_distr [lemma, in Coq.PArith.BinPos]
Pos.succ_le_mono [lemma, in Coq.PArith.BinPos]
Pos.succ_lt_mono [lemma, in Coq.PArith.BinPos]
Pos.succ_inj [lemma, in Coq.PArith.BinPos]
Pos.succ_pred [lemma, in Coq.PArith.BinPos]
Pos.succ_pred_or [lemma, in Coq.PArith.BinPos]
Pos.succ_not_1 [lemma, in Coq.PArith.BinPos]
Pos.succ_pred_double [lemma, in Coq.PArith.BinPos]
Pos.succ_discr [lemma, in Coq.PArith.BinPos]
Pos.switch_Eq [definition, in Coq.PArith.BinPos]
Pos.t [definition, in Coq.PArith.BinPosDef]
Pos.ten [abbreviation, in Coq.PArith.BinPosDef]
Pos.testbit [definition, in Coq.PArith.BinPosDef]
Pos.testbit_nat [definition, in Coq.PArith.BinPosDef]
Pos.to_int [definition, in Coq.PArith.BinPosDef]
Pos.to_uint [definition, in Coq.PArith.BinPosDef]
Pos.to_little_uint [definition, in Coq.PArith.BinPosDef]
Pos.to_nat [definition, in Coq.PArith.BinPosDef]
Pos.xI_succ_xO [lemma, in Coq.PArith.BinPos]
( _ | _ ) (positive_scope) [notation, in Coq.PArith.BinPosDef]
_ [notation, in Coq.PArith.BinPosDef]
_ <=? _ (positive_scope) [notation, in Coq.PArith.BinPosDef]
_ =? _ (positive_scope) [notation, in Coq.PArith.BinPosDef]
_ ?= _ (positive_scope) [notation, in Coq.PArith.BinPosDef]
_ ^ _ (positive_scope) [notation, in Coq.PArith.BinPosDef]
_ * _ (positive_scope) [notation, in Coq.PArith.BinPosDef]
_ - _ (positive_scope) [notation, in Coq.PArith.BinPosDef]
_ + _ (positive_scope) [notation, in Coq.PArith.BinPosDef]
_ < _ <= _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ < _ < _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ <= _ < _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ <= _ <= _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ > _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ >= _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ < _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ <= _ (positive_scope) [notation, in Coq.PArith.BinPos]
Pos2Nat [module, in Coq.PArith.Pnat]
Pos2Nat.id [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_iter [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_max [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_min [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_pred_max [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_pred [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_sub_max [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_sub [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_ge [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_gt [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_le [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_lt [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_compare [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_iff [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_xI [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_xO [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_1 [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_mul [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_add [lemma, in Coq.PArith.Pnat]
Pos2Nat.inj_succ [lemma, in Coq.PArith.Pnat]
Pos2Nat.is_pos [lemma, in Coq.PArith.Pnat]
Pos2Nat.is_succ [lemma, in Coq.PArith.Pnat]
Pos2SuccNat [module, in Coq.PArith.Pnat]
Pos2SuccNat.id_succ [lemma, in Coq.PArith.Pnat]
Pos2SuccNat.pred_id [lemma, in Coq.PArith.Pnat]
Pos2Z [module, in Coq.ZArith.BinInt]
Pos2Z.add_pos_pos [lemma, in Coq.ZArith.BinInt]
Pos2Z.add_neg_pos [lemma, in Coq.ZArith.BinInt]
Pos2Z.add_pos_neg [lemma, in Coq.ZArith.BinInt]
Pos2Z.add_neg_neg [lemma, in Coq.ZArith.BinInt]
Pos2Z.divide_pos_neg_l [lemma, in Coq.ZArith.BinInt]
Pos2Z.divide_pos_neg_r [lemma, in Coq.ZArith.BinInt]
Pos2Z.id [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_pos_iff [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_pos [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_neg_iff [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_neg [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_testbit [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_divide [definition, in Coq.ZArith.BinInt]
Pos2Z.inj_gcd [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_sqrt [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_min [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_max [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_eqb [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_ltb [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_leb [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_compare [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_square [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_pow [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_pow_pos [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_mul [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_pred [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_sub_max [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_sub [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_add [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_succ [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_xI [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_xO [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_1 [lemma, in Coq.ZArith.BinInt]
Pos2Z.inj_iff [lemma, in Coq.ZArith.BinInt]
Pos2Z.is_nonneg [lemma, in Coq.ZArith.BinInt]
Pos2Z.is_pos [lemma, in Coq.ZArith.BinInt]
Pos2Z.neg_xI [lemma, in Coq.ZArith.BinInt]
Pos2Z.neg_xO [lemma, in Coq.ZArith.BinInt]
Pos2Z.neg_lt_neg [lemma, in Coq.ZArith.BinInt]
Pos2Z.neg_le_neg [lemma, in Coq.ZArith.BinInt]
Pos2Z.neg_lt_pos [lemma, in Coq.ZArith.BinInt]
Pos2Z.neg_le_pos [lemma, in Coq.ZArith.BinInt]
Pos2Z.neg_is_nonpos [lemma, in Coq.ZArith.BinInt]
Pos2Z.neg_is_neg [lemma, in Coq.ZArith.BinInt]
Pos2Z.opp_pos [lemma, in Coq.ZArith.BinInt]
Pos2Z.opp_neg [lemma, in Coq.ZArith.BinInt]
Pos2Z.pos_xI [lemma, in Coq.ZArith.BinInt]
Pos2Z.pos_xO [lemma, in Coq.ZArith.BinInt]
Pos2Z.pos_lt_pos [lemma, in Coq.ZArith.BinInt]
Pos2Z.pos_le_pos [lemma, in Coq.ZArith.BinInt]
Pos2Z.pos_is_nonneg [lemma, in Coq.ZArith.BinInt]
Pos2Z.pos_is_pos [lemma, in Coq.ZArith.BinInt]
Pos2Z.testbit_pos [lemma, in Coq.ZArith.BinInt]
Pos2Z.testbit_neg [lemma, in Coq.ZArith.BinInt]
pow [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
pow [definition, in Coq.setoid_ring.Integral_domain]
pow [definition, in Coq.Init.Nat]
pow [definition, in Coq.Logic.Berardi]
Pow [module, in Coq.Numbers.NatInt.NZPow]
Pow [definition, in Coq.Relations.Relation_Operators]
pow [definition, in Coq.Reals.Rpow_def]
power [projection, in Coq.setoid_ring.Algebra_syntax]
Power [record, in Coq.setoid_ring.Algebra_syntax]
power [constructor, in Coq.setoid_ring.Algebra_syntax]
Power [inductive, in Coq.setoid_ring.Algebra_syntax]
Power [abbreviation, in Coq.Wellfounded.Lexicographic_Exponentiation]
Power [section, in Coq.setoid_ring.Ring_theory]
powerRZ [definition, in Coq.Reals.Rfunctions]
PowerRZ [section, in Coq.Reals.Rfunctions]
powerRZ_mult_distr [lemma, in Coq.Reals.Rfunctions]
powerRZ_neg [lemma, in Coq.Reals.Rfunctions]
powerRZ_inv [lemma, in Coq.Reals.Rfunctions]
powerRZ_ind [lemma, in Coq.Reals.Rfunctions]
powerRZ_R1 [lemma, in Coq.Reals.Rfunctions]
powerRZ_le [lemma, in Coq.Reals.Rfunctions]
powerRZ_lt [lemma, in Coq.Reals.Rfunctions]
powerRZ_add [lemma, in Coq.Reals.Rfunctions]
powerRZ_pos_sub [lemma, in Coq.Reals.Rfunctions]
powerRZ_NOR [lemma, in Coq.Reals.Rfunctions]
powerRZ_1 [lemma, in Coq.Reals.Rfunctions]
powerRZ_O [lemma, in Coq.Reals.Rfunctions]
powerRZ_Rpower [lemma, in Coq.Reals.Rpower]
PowerRZ.Z_compl [section, in Coq.Reals.Rfunctions]
_ ^Z _ (R_scope) [notation, 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_ring [instance, in Coq.setoid_ring.Ncring]
Power_monotonic [lemma, in Coq.Reals.Rfunctions]
power_theory [record, in Coq.setoid_ring.Ncring_polynom]
power_theory [record, in Coq.setoid_ring.Ring_theory]
Power_set_PO [definition, in Coq.Sets.Powerset]
Power_set_Inhabited [lemma, in Coq.Sets.Powerset]
Power_set [inductive, in Coq.Sets.Powerset]
Power.mul_assoc [variable, in Coq.setoid_ring.Ring_theory]
Power.mul_ext [variable, in Coq.setoid_ring.Ring_theory]
Power.R [variable, in Coq.setoid_ring.Ring_theory]
Power.req [variable, in Coq.setoid_ring.Ring_theory]
Power.rI [variable, in Coq.setoid_ring.Ring_theory]
Power.rmul [variable, in Coq.setoid_ring.Ring_theory]
Power.Rsth [variable, in Coq.setoid_ring.Ring_theory]
_ == _ [notation, in Coq.setoid_ring.Ring_theory]
_ * _ [notation, in Coq.setoid_ring.Ring_theory]
PowNotation [module, in Coq.Numbers.NatInt.NZPow]
_ ^ _ [notation, in Coq.Numbers.NatInt.NZPow]
pow_pos_add [lemma, in Coq.micromega.EnvRing]
pow_succ_r [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
pow_0_r [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
pow_IZR [lemma, in Coq.Reals.RIneq]
pow_INR [lemma, in Coq.Reals.RIneq]
pow_i [lemma, in Coq.Reals.Rtrigo_def]
pow_2_n_infty [lemma, in Coq.Reals.Rsqrt_def]
pow_2_n_growing [lemma, in Coq.Reals.Rsqrt_def]
pow_2_n_neq_R0 [lemma, in Coq.Reals.Rsqrt_def]
pow_2_n [definition, in Coq.Reals.Rsqrt_def]
pow_fct [definition, in Coq.Reals.Ranalysis1]
pow_pos_div [lemma, in Coq.setoid_ring.Field_theory]
pow_pos_nz [lemma, in Coq.setoid_ring.Field_theory]
pow_pos_mul_r [lemma, in Coq.setoid_ring.Field_theory]
pow_pos_add_r [lemma, in Coq.setoid_ring.Field_theory]
pow_pos_mul_l [lemma, in Coq.setoid_ring.Field_theory]
pow_pos_cst [lemma, in Coq.setoid_ring.Field_theory]
pow_pos_1 [lemma, in Coq.setoid_ring.Field_theory]
pow_pos_0 [lemma, in Coq.setoid_ring.Field_theory]
pow_N_ext [instance, in Coq.setoid_ring.Field_theory]
pow_ext [instance, in Coq.setoid_ring.Field_theory]
pow_not_zero [lemma, in Coq.setoid_ring.Integral_domain]
pow_N_pow_N [lemma, in Coq.setoid_ring.Ncring]
pow_pos_add [lemma, in Coq.setoid_ring.Ncring]
pow_pos_succ [lemma, in Coq.setoid_ring.Ncring]
pow_pos_comm [lemma, in Coq.setoid_ring.Ncring]
pow_N [definition, in Coq.setoid_ring.Ncring]
pow_pos [definition, in Coq.setoid_ring.Ncring]
pow_powerRZ [lemma, in Coq.Reals.Rfunctions]
pow_maj_Rabs [lemma, in Coq.Reals.Rfunctions]
pow_Rabs [lemma, in Coq.Reals.Rfunctions]
pow_R1_Rle [lemma, in Coq.Reals.Rfunctions]
pow_incr [lemma, in Coq.Reals.Rfunctions]
pow_mult [lemma, in Coq.Reals.Rfunctions]
pow_1_abs [lemma, in Coq.Reals.Rfunctions]
pow_1_odd [lemma, in Coq.Reals.Rfunctions]
pow_1_even [lemma, in Coq.Reals.Rfunctions]
pow_le [lemma, in Coq.Reals.Rfunctions]
pow_Rsqr [lemma, in Coq.Reals.Rfunctions]
pow_R1 [lemma, in Coq.Reals.Rfunctions]
pow_lt_1_zero [lemma, in Coq.Reals.Rfunctions]
pow_ne_zero [lemma, in Coq.Reals.Rfunctions]
Pow_x_infinity [lemma, in Coq.Reals.Rfunctions]
pow_lt [lemma, in Coq.Reals.Rfunctions]
pow_RN_plus [lemma, in Coq.Reals.Rfunctions]
pow_nonzero [lemma, in Coq.Reals.Rfunctions]
pow_add [lemma, in Coq.Reals.Rfunctions]
pow_1 [lemma, in Coq.Reals.Rfunctions]
pow_O [lemma, in Coq.Reals.Rfunctions]
pow_N_gen [definition, in Coq.setoid_ring.Ncring_polynom]
pow_pos_gen [definition, in Coq.setoid_ring.Ncring_polynom]
pow_sqr [lemma, in Coq.Reals.Cos_rel]
pow_pos_add [lemma, in Coq.setoid_ring.Ring_polynom]
pow_lt_1_compat [lemma, in Coq.Reals.Ratan]
pow_N_th [definition, in Coq.setoid_ring.Ring_theory]
pow_N_pow_N [lemma, in Coq.setoid_ring.Ring_theory]
pow_N [definition, in Coq.setoid_ring.Ring_theory]
pow_pos_add [lemma, in Coq.setoid_ring.Ring_theory]
pow_pos_succ [lemma, in Coq.setoid_ring.Ring_theory]
pow_pos_swap [lemma, in Coq.setoid_ring.Ring_theory]
pow_pos [definition, in Coq.setoid_ring.Ring_theory]
Pow' [module, in Coq.Numbers.NatInt.NZPow]
Pow.pow [axiom, in Coq.Numbers.NatInt.NZPow]
pow1 [lemma, in Coq.Reals.Rfunctions]
pow2_abs [lemma, in Coq.Reals.Ratan]
pow2_ge_0 [lemma, in Coq.Reals.Ratan]
PO_cond2 [projection, in Coq.Sets.Partial_Order]
PO_cond1 [projection, in Coq.Sets.Partial_Order]
PO_of_chain [projection, in Coq.Sets.Cpo]
PO_of_cpo [projection, in Coq.Sets.Cpo]
Pphi [definition, in Coq.micromega.EnvRing]
Pphi [definition, in Coq.setoid_ring.Ncring_polynom]
Pphi [definition, in Coq.setoid_ring.Ring_polynom]
Pphi_dev_ok [lemma, in Coq.setoid_ring.Ring_polynom]
Pphi_dev [definition, in Coq.setoid_ring.Ring_polynom]
Pphi_pow_ok [lemma, in Coq.setoid_ring.Ring_polynom]
Pphi_pow [definition, in Coq.setoid_ring.Ring_polynom]
Pphi_avoid_ok [lemma, in Coq.setoid_ring.Ring_polynom]
Pphi_avoid [definition, in Coq.setoid_ring.Ring_polynom]
Pphi_ext [instance, in Coq.setoid_ring.Ring_polynom]
Pphi0 [lemma, in Coq.micromega.EnvRing]
Pphi0 [lemma, in Coq.setoid_ring.Ncring_polynom]
Pphi0 [lemma, in Coq.setoid_ring.Ring_polynom]
Pphi1 [lemma, in Coq.micromega.EnvRing]
Pphi1 [lemma, in Coq.setoid_ring.Ncring_polynom]
Pphi1 [lemma, in Coq.setoid_ring.Ring_polynom]
Pplength [definition, in Coq.NArith.Ndist]
Pplus [abbreviation, in Coq.PArith.BinPos]
Pplus_minus [lemma, in Coq.PArith.BinPos]
Pplus_one_succ_l [lemma, in Coq.PArith.BinPos]
Pplus_one_succ_r [lemma, in Coq.PArith.BinPos]
Pplus_minus_assoc [abbreviation, in Coq.PArith.BinPos]
Pplus_minus_eq [abbreviation, in Coq.PArith.BinPos]
Pplus_le_mono [abbreviation, in Coq.PArith.BinPos]
Pplus_le_mono_r [abbreviation, in Coq.PArith.BinPos]
Pplus_le_mono_l [abbreviation, in Coq.PArith.BinPos]
Pplus_lt_mono [abbreviation, in Coq.PArith.BinPos]
Pplus_lt_mono_r [abbreviation, in Coq.PArith.BinPos]
Pplus_lt_mono_l [abbreviation, in Coq.PArith.BinPos]
Pplus_compare_mono_r [abbreviation, in Coq.PArith.BinPos]
Pplus_compare_mono_l [abbreviation, in Coq.PArith.BinPos]
Pplus_diag [abbreviation, in Coq.PArith.BinPos]
Pplus_xO_double_minus_one [abbreviation, in Coq.PArith.BinPos]
Pplus_xI_double_minus_one [abbreviation, in Coq.PArith.BinPos]
Pplus_xO [abbreviation, in Coq.PArith.BinPos]
Pplus_assoc [abbreviation, in Coq.PArith.BinPos]
Pplus_carry_reg_l [abbreviation, in Coq.PArith.BinPos]
Pplus_carry_reg_r [abbreviation, in Coq.PArith.BinPos]
Pplus_reg_l [abbreviation, in Coq.PArith.BinPos]
Pplus_reg_r [abbreviation, in Coq.PArith.BinPos]
Pplus_carry_plus [abbreviation, in Coq.PArith.BinPos]
Pplus_no_neutral [abbreviation, in Coq.PArith.BinPos]
Pplus_succ_permute_l [abbreviation, in Coq.PArith.BinPos]
Pplus_succ_permute_r [abbreviation, in Coq.PArith.BinPos]
Pplus_comm [abbreviation, in Coq.PArith.BinPos]
Pplus_carry_spec [abbreviation, in Coq.PArith.BinPos]
Pplus_carry [abbreviation, in Coq.PArith.BinPos]
Pplus_plus [abbreviation, in Coq.PArith.Pnat]
Ppow [abbreviation, in Coq.PArith.BinPos]
Ppow_N_ok [lemma, in Coq.micromega.EnvRing]
Ppow_pos_ok [lemma, in Coq.micromega.EnvRing]
Ppow_N [definition, in Coq.micromega.EnvRing]
Ppow_pos [definition, in Coq.micromega.EnvRing]
Ppow_gt_1 [abbreviation, in Coq.PArith.BinPos]
Ppow_succ_r [abbreviation, in Coq.PArith.BinPos]
Ppow_1_r [abbreviation, in Coq.PArith.BinPos]
Ppow_N_ok [lemma, in Coq.setoid_ring.Ncring_polynom]
Ppow_pos_ok [lemma, in Coq.setoid_ring.Ncring_polynom]
Ppow_N [definition, in Coq.setoid_ring.Ncring_polynom]
Ppow_pos [definition, in Coq.setoid_ring.Ncring_polynom]
Ppow_N_ok [lemma, in Coq.setoid_ring.Ring_polynom]
Ppow_pos_ok [lemma, in Coq.setoid_ring.Ring_polynom]
Ppow_N [definition, in Coq.setoid_ring.Ring_polynom]
Ppow_pos [definition, in Coq.setoid_ring.Ring_polynom]
Ppred [abbreviation, in Coq.PArith.BinPos]
Ppred_minus [lemma, in Coq.PArith.BinPos]
Ppred_mask [abbreviation, in Coq.PArith.BinPos]
Ppred_succ [abbreviation, in Coq.PArith.BinPos]
Ppred_Nsucc [abbreviation, in Coq.NArith.BinNat]
Ppred_N_spec [abbreviation, in Coq.NArith.BinNat]
Ppred_N [abbreviation, in Coq.NArith.BinNat]
pre [projection, in Coq.Reals.RiemannInt_SF]
Prec [abbreviation, in Coq.PArith.BinPos]
Prect [abbreviation, in Coq.PArith.BinPos]
Prect_base [abbreviation, in Coq.PArith.BinPos]
Prect_succ [abbreviation, in Coq.PArith.BinPos]
pred [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
pred [definition, in Coq.ssr.ssrbool]
pred [definition, in Coq.Init.Nat]
pred [abbreviation, in Coq.Init.Peano]
predArgType [definition, in Coq.ssr.ssrbool]
predC [definition, in Coq.ssr.ssrbool]
predD [definition, in Coq.ssr.ssrbool]
PredExt_RelChoice_imp_EM.rel_choice [variable, in Coq.Logic.Diaconescu]
PredExt_RelChoice_imp_EM.pred_extensionality [variable, in Coq.Logic.Diaconescu]
PredExt_RelChoice_imp_EM [section, in Coq.Logic.Diaconescu]
PredExt_imp_PropFunExt [lemma, in Coq.Logic.PropExtensionalityFacts]
PredExt_imp_PropExt [lemma, in Coq.Logic.PropExtensionalityFacts]
predI [definition, in Coq.ssr.ssrbool]
predicate [abbreviation, in Coq.Classes.RelationClasses]
PredicateExtensionality [definition, in Coq.Logic.Diaconescu]
PredicateExtensionality [abbreviation, in Coq.Logic.PropExtensionalityFacts]
Predicates [section, in Coq.ssr.ssrbool]
Predicates.T [variable, in Coq.ssr.ssrbool]
predicate_implication_pointwise [lemma, in Coq.Classes.Morphisms_Relations]
predicate_equivalence_pointwise [lemma, in Coq.Classes.Morphisms_Relations]
predicate_implication_preorder [instance, in Coq.Classes.RelationClasses]
predicate_equivalence_equivalence [instance, in Coq.Classes.RelationClasses]
predicate_union [definition, in Coq.Classes.RelationClasses]
predicate_intersection [definition, in Coq.Classes.RelationClasses]
predicate_implication [definition, in Coq.Classes.RelationClasses]
predicate_equivalence [definition, in Coq.Classes.RelationClasses]
predicate_exists [definition, in Coq.Classes.RelationClasses]
predicate_all [definition, in Coq.Classes.RelationClasses]
predT [definition, in Coq.ssr.ssrbool]
predType [record, in Coq.ssr.ssrbool]
PredType [constructor, in Coq.ssr.ssrbool]
predU [definition, in Coq.ssr.ssrbool]
pred_of_minus [lemma, in Coq.Arith.Minus]
pred_ext_and_rel_choice_imp_EM [lemma, in Coq.Logic.Diaconescu]
pred_c [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
pred_key [inductive, in Coq.ssr.ssrbool]
pred_class [abbreviation, in Coq.ssr.ssrbool]
pred_sort [projection, in Coq.ssr.ssrbool]
pred_Sn [lemma, in Coq.Init.Peano]
pred_o_P_of_succ_nat_o_nat_of_P_eq_id [abbreviation, in Coq.PArith.Pnat]
pred0 [definition, in Coq.ssr.ssrbool]
prefix [definition, in Coq.Strings.String]
prefix_correct [lemma, in Coq.Strings.String]
preim [definition, in Coq.ssr.ssrbool]
Prelude [library]
PreOmega [library]
PreOrder [record, in Coq.Classes.CRelationClasses]
Preorder [inductive, in Coq.Sets.Relations_1]
preorder [record, in Coq.Relations.Relation_Definitions]
PreOrder [record, in Coq.Classes.RelationClasses]
PreOrder_Transitive [projection, in Coq.Classes.CRelationClasses]
PreOrder_Reflexive [projection, in Coq.Classes.CRelationClasses]
PreOrder_Transitive [projection, in Coq.Classes.RelationClasses]
PreOrder_Reflexive [projection, in Coq.Classes.RelationClasses]
preord_trans [projection, in Coq.Relations.Relation_Definitions]
preord_refl [projection, in Coq.Relations.Relation_Definitions]
PreWeakKonigsLemma [lemma, in Coq.Logic.WKL]
pre_symmetric [definition, in Coq.ssr.ssrbool]
pre_cos_bound [lemma, in Coq.Reals.Rtrigo_alt]
pre_sin_bound [lemma, in Coq.Reals.Rtrigo_alt]
pre_atan [definition, in Coq.Reals.Ratan]
prime [inductive, in Coq.ZArith.Znumtheory]
prime_dec [definition, in Coq.ZArith.Znumtheory]
prime_dec_aux [definition, in Coq.ZArith.Znumtheory]
prime_div_prime [lemma, in Coq.ZArith.Znumtheory]
prime_alt [lemma, in Coq.ZArith.Znumtheory]
prime_ge_2 [lemma, in Coq.ZArith.Znumtheory]
prime_3 [lemma, in Coq.ZArith.Znumtheory]
prime_2 [lemma, in Coq.ZArith.Znumtheory]
prime_mult [lemma, in Coq.ZArith.Znumtheory]
prime_rel_prime [lemma, in Coq.ZArith.Znumtheory]
prime_divisors [lemma, in Coq.ZArith.Znumtheory]
prime_intro [constructor, in Coq.ZArith.Znumtheory]
prime_power_prime [lemma, in Coq.ZArith.Zpow_facts]
prime' [definition, 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_uncurry [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]
prod_SO_Rle [lemma, in Coq.Reals.Rprod]
prod_SO_pos [lemma, in Coq.Reals.Rprod]
prod_SO_split [lemma, in Coq.Reals.Rprod]
prod_f_SO [abbreviation, in Coq.Reals.Rprod]
prod_f_R0 [definition, in Coq.Reals.Rprod]
prod_neq_R0 [abbreviation, in Coq.Reals.RIneq]
prod_eqdec [instance, in Coq.Classes.SetoidDec]
prod_curry [definition, in Coq.Init.Datatypes]
prod_uncurry [definition, in Coq.Init.Datatypes]
prod_pos_nat [definition, in Coq.micromega.ZMicromega]
prod_curry_uncurry [lemma, in Coq.Program.Combinators]
prod_uncurry_curry [lemma, in Coq.Program.Combinators]
prod_length [lemma, in Coq.Lists.List]
prod_eqdec [instance, in Coq.Classes.EquivDec]
Program [library]
project [lemma, in Coq.rtauto.Rtauto]
Projections [section, in Coq.Init.Specif]
projections [section, in Coq.Init.Datatypes]
Projections.A [variable, in Coq.Init.Specif]
Projections.P [variable, in Coq.Init.Specif]
Projections2 [section, in Coq.Init.Specif]
Projections2.A [variable, in Coq.Init.Specif]
Projections2.P [variable, in Coq.Init.Specif]
Projections2.Q [variable, in Coq.Init.Specif]
project_In [lemma, in Coq.rtauto.Rtauto]
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]
projT1_of_sigT2_eq [definition, in Coq.Init.Specif]
projT1_eq [definition, in Coq.Init.Specif]
projT2 [definition, in Coq.Init.Specif]
projT2_of_sigT2_eq [definition, in Coq.Init.Specif]
projT2_eq [definition, in Coq.Init.Specif]
projT3 [definition, in Coq.Init.Specif]
projT3_eq [definition, in Coq.Init.Specif]
proj1 [lemma, in Coq.Init.Logic]
proj1_inf [definition, in Coq.Logic.ChoiceFacts]
proj1_sig_of_sig2_eq [definition, in Coq.Init.Specif]
proj1_sig_eq [definition, in Coq.Init.Specif]
proj1_sig [definition, in Coq.Init.Specif]
proj2 [lemma, in Coq.Init.Logic]
proj2_sig_of_sig2_eq [definition, in Coq.Init.Specif]
proj2_sig_eq [definition, in Coq.Init.Specif]
proj2_sig [definition, in Coq.Init.Specif]
proj3_sig_eq [definition, in Coq.Init.Specif]
proj3_sig [definition, in Coq.Init.Specif]
prolongement_C0 [lemma, in Coq.Reals.Rtopology]
proof [inductive, in Coq.rtauto.Rtauto]
ProofIrrelevance [definition, in Coq.Logic.ChoiceFacts]
ProofIrrelevance [module, in Coq.Logic.ProofIrrelevanceFacts]
ProofIrrelevance [library]
ProofIrrelevanceFacts [library]
ProofIrrelevanceTheory [module, in Coq.Logic.ProofIrrelevanceFacts]
ProofIrrelevanceTheory [module, in Coq.Logic.ProofIrrelevance]
ProofIrrelevanceTheory.EqdepTheory [module, in Coq.Logic.ProofIrrelevanceFacts]
ProofIrrelevanceTheory.eq_indd [definition, in Coq.Logic.ProofIrrelevanceFacts]
ProofIrrelevanceTheory.Eq_rect_eq.eq_rect_eq [lemma, in Coq.Logic.ProofIrrelevanceFacts]
ProofIrrelevanceTheory.Eq_rect_eq [module, 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.a2 [variable, in Coq.Logic.Diaconescu]
ProofIrrel_RelChoice_imp_EqEM.a1 [variable, in Coq.Logic.Diaconescu]
ProofIrrel_RelChoice_imp_EqEM.A [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]
ProofIrrel_RelChoice_imp_EqEM [section, in Coq.Logic.Diaconescu]
proof_irrelevance [lemma, in Coq.Logic.Classical_Prop]
proof_admitted [axiom, in Coq.Compat.AdmitAxiom]
proof_irrel_rel_choice_imp_eq_dec' [lemma, in Coq.Logic.Diaconescu]
proof_irrel_rel_choice_imp_eq_dec [lemma, in Coq.Logic.Diaconescu]
proof_irrel [lemma, in Coq.Logic.Diaconescu]
proof_irrelevance_cci [lemma, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_CCI.em [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_CCI [section, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_WEM_CC.b2p [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_WEM_CC.p2b [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_WEM_CC.b2 [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_WEM_CC.b1 [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_WEM_CC.B [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_WEM_CC.wem [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_WEM_CC.or_dep_elim [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_WEM_CC.or_elim_redr [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_WEM_CC.or_elim_redl [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_WEM_CC.or_elim [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_WEM_CC.or_intror [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_WEM_CC.or_introl [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_WEM_CC.or [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_WEM_CC [section, in Coq.Logic.ClassicalFacts]
proof_irrelevance_cc [lemma, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.b2p [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.p2b [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.b2 [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.b1 [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.B [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.em [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.or_dep_elim [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.or_elim_redr [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.or_elim_redl [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.or_elim [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.or_intror [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.or_introl [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC.or [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_EM_CC [section, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_CIC [section, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_Prop_Ext_CC [section, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_gen.bool_dep_induction [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_gen.bool_elim_redr [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_gen.bool_elim_redl [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_gen.bool_elim [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_gen.bool [variable, in Coq.Logic.ClassicalFacts]
Proof_irrelevance_gen [section, in Coq.Logic.ClassicalFacts]
proof_irrelevance [definition, in Coq.Logic.ClassicalFacts]
proof_irrelevance [axiom, in Coq.Logic.ProofIrrelevance]
proof_irrelevance [lemma, in Coq.Logic.PropExtensionality]
propagate [constructor, in Coq.Logic.WeakFan]
propagate_at [constructor, in Coq.Logic.WKL]
Proper [record, in Coq.Classes.Morphisms]
Proper [inductive, in Coq.Classes.Morphisms]
Proper [section, in Coq.Classes.Morphisms]
Proper [record, in Coq.Classes.CMorphisms]
Proper [inductive, in Coq.Classes.CMorphisms]
Proper [section, in Coq.Classes.CMorphisms]
ProperNotations [module, in Coq.Classes.Morphisms]
ProperNotations [module, in Coq.Classes.CMorphisms]
_ --> _ (signature_scope) [notation, in Coq.Classes.Morphisms]
_ ==> _ (signature_scope) [notation, in Coq.Classes.Morphisms]
_ ++> _ (signature_scope) [notation, in Coq.Classes.Morphisms]
_ --> _ (signature_scope) [notation, in Coq.Classes.CMorphisms]
_ ==> _ (signature_scope) [notation, in Coq.Classes.CMorphisms]
_ ++> _ (signature_scope) [notation, in Coq.Classes.CMorphisms]
ProperProxy [record, in Coq.Classes.Morphisms]
ProperProxy [inductive, in Coq.Classes.Morphisms]
ProperProxy [record, in Coq.Classes.CMorphisms]
ProperProxy [inductive, in Coq.Classes.CMorphisms]
Properties [module, in Coq.FSets.FMapFacts]
Properties [section, in Coq.Relations.Operators_Properties]
Properties [module, in Coq.MSets.MSetProperties]
Properties [module, in Coq.FSets.FSetProperties]
Properties.A [variable, in Coq.Relations.Operators_Properties]
Properties.Clos_Refl_Sym_Trans [section, in Coq.Relations.Operators_Properties]
_ * [notation, 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]
proper_sym_impl_iff_2 [lemma, in Coq.Classes.Morphisms]
proper_sym_impl_iff [lemma, in Coq.Classes.Morphisms]
proper_sym_flip_2 [lemma, in Coq.Classes.Morphisms]
proper_sym_flip [lemma, in Coq.Classes.Morphisms]
proper_normalizes_proper [lemma, in Coq.Classes.Morphisms]
proper_proper [instance, in Coq.Classes.Morphisms]
proper_eq [lemma, in Coq.Classes.Morphisms]
proper_flip_proper [definition, in Coq.Classes.Morphisms]
proper_subrelation_proper [instance, in Coq.Classes.Morphisms]
proper_proper_proxy [lemma, in Coq.Classes.Morphisms]
proper_proxy [projection, in Coq.Classes.Morphisms]
proper_proxy [constructor, in Coq.Classes.Morphisms]
proper_prf [projection, in Coq.Classes.Morphisms]
proper_prf [constructor, in Coq.Classes.Morphisms]
proper_sym_arrow_iffT_2 [lemma, in Coq.Classes.CMorphisms]
proper_sym_impl_iff_2 [lemma, in Coq.Classes.CMorphisms]
proper_sym_arrow_iffT [lemma, in Coq.Classes.CMorphisms]
proper_sym_impl_iff [lemma, in Coq.Classes.CMorphisms]
proper_sym_flip_2 [lemma, in Coq.Classes.CMorphisms]
proper_sym_flip [lemma, in Coq.Classes.CMorphisms]
proper_normalizes_proper [lemma, in Coq.Classes.CMorphisms]
proper_proper [instance, in Coq.Classes.CMorphisms]
proper_eq [lemma, in Coq.Classes.CMorphisms]
proper_flip_proper [definition, in Coq.Classes.CMorphisms]
proper_subrelation_proper_arrow [instance, in Coq.Classes.CMorphisms]
proper_proper_proxy [lemma, in Coq.Classes.CMorphisms]
proper_proxy [projection, in Coq.Classes.CMorphisms]
proper_proxy [constructor, in Coq.Classes.CMorphisms]
proper_prf [projection, in Coq.Classes.CMorphisms]
proper_prf [constructor, in Coq.Classes.CMorphisms]
Proper.U [variable, in Coq.Classes.Morphisms]
PropExtensionality [library]
PropExtensionalityFacts [library]
PropExt_imp_RefutPropExt [lemma, in Coq.Logic.PropExtensionalityFacts]
PropExt_imp_ProvPropExt [lemma, in Coq.Logic.PropExtensionalityFacts]
PropExt_and_PropFunExt_iff_PredExt [lemma, in Coq.Logic.PropExtensionalityFacts]
PropExt_and_PropFunExt_imp_PredExt [lemma, in Coq.Logic.PropExtensionalityFacts]
PropFacts [library]
PropNeqType [module, in Coq.Logic.Hurkens]
PropNeqType.paradox [lemma, in Coq.Logic.Hurkens]
PropositionalExtensionality [abbreviation, in Coq.Logic.PropExtensionalityFacts]
PropositionalFunctionalExtensionality [abbreviation, in Coq.Logic.PropExtensionalityFacts]
propositional_extensionality [axiom, in Coq.Logic.PropExtensionality]
Props [module, in Coq.MSets.MSetGenTree]
Props.BSLeaf [constructor, in Coq.MSets.MSetGenTree]
Props.BSNode [constructor, in Coq.MSets.MSetGenTree]
Props.bst [inductive, in Coq.MSets.MSetGenTree]
Props.bst_ind [definition, in Coq.MSets.MSetGenTree]
Props.bst_Ok [instance, in Coq.MSets.MSetGenTree]
Props.cardinal_spec [definition, in Coq.MSets.MSetGenTree]
Props.choose_spec3 [lemma, in Coq.MSets.MSetGenTree]
Props.choose_spec2 [lemma, in Coq.MSets.MSetGenTree]
Props.choose_spec1 [lemma, in Coq.MSets.MSetGenTree]
Props.Cmp [definition, in Coq.MSets.MSetGenTree]
Props.compare_spec [lemma, in Coq.MSets.MSetGenTree]
Props.compare_Cmp [lemma, in Coq.MSets.MSetGenTree]
Props.compare_cont_Cmp [lemma, in Coq.MSets.MSetGenTree]
Props.compare_more_Cmp [lemma, in Coq.MSets.MSetGenTree]
Props.compare_end_Cmp [lemma, in Coq.MSets.MSetGenTree]
Props.cons_1 [lemma, in Coq.MSets.MSetGenTree]
Props.elements_sort_ok [lemma, in Coq.MSets.MSetGenTree]
Props.elements_node [lemma, in Coq.MSets.MSetGenTree]
Props.elements_app [lemma, in Coq.MSets.MSetGenTree]
Props.elements_cardinal [lemma, in Coq.MSets.MSetGenTree]
Props.elements_aux_cardinal [lemma, in Coq.MSets.MSetGenTree]
Props.elements_spec2w [lemma, in Coq.MSets.MSetGenTree]
Props.elements_spec2 [lemma, in Coq.MSets.MSetGenTree]
Props.elements_spec2' [lemma, in Coq.MSets.MSetGenTree]
Props.elements_spec1 [lemma, in Coq.MSets.MSetGenTree]
Props.elements_spec1' [lemma, in Coq.MSets.MSetGenTree]
Props.Empty [definition, in Coq.MSets.MSetGenTree]
Props.empty_ok [instance, in Coq.MSets.MSetGenTree]
Props.empty_spec [lemma, in Coq.MSets.MSetGenTree]
Props.eq [definition, in Coq.MSets.MSetGenTree]
Props.Equal [definition, in Coq.MSets.MSetGenTree]
Props.equal_spec [lemma, in Coq.MSets.MSetGenTree]
Props.eq_Leq [lemma, in Coq.MSets.MSetGenTree]
Props.eq_equiv [instance, in Coq.MSets.MSetGenTree]
Props.Exists [definition, in Coq.MSets.MSetGenTree]
Props.exists_spec [lemma, in Coq.MSets.MSetGenTree]
Props.flatten_e_elements [lemma, in Coq.MSets.MSetGenTree]
Props.flatten_e [definition, in Coq.MSets.MSetGenTree]
Props.fold_spec [lemma, in Coq.MSets.MSetGenTree]
Props.fold_spec' [lemma, in Coq.MSets.MSetGenTree]
Props.for_all_spec [lemma, in Coq.MSets.MSetGenTree]
Props.For_all [definition, in Coq.MSets.MSetGenTree]
Props.gtb_tree_iff [lemma, in Coq.MSets.MSetGenTree]
Props.gtb_tree [definition, in Coq.MSets.MSetGenTree]
Props.gt_tree_compat [instance, in Coq.MSets.MSetGenTree]
Props.gt_tree_trans [lemma, in Coq.MSets.MSetGenTree]
Props.gt_tree_not_in [lemma, in Coq.MSets.MSetGenTree]
Props.gt_tree_node [lemma, in Coq.MSets.MSetGenTree]
Props.gt_leaf [lemma, in Coq.MSets.MSetGenTree]
Props.gt_tree [definition, in Coq.MSets.MSetGenTree]
Props.In [definition, in Coq.MSets.MSetGenTree]
Props.InLeft [constructor, in Coq.MSets.MSetGenTree]
Props.InRight [constructor, in Coq.MSets.MSetGenTree]
Props.InT [inductive, in Coq.MSets.MSetGenTree]
Props.In_leaf_iff [lemma, in Coq.MSets.MSetGenTree]
Props.In_node_iff [lemma, in Coq.MSets.MSetGenTree]
Props.In_compat [instance, in Coq.MSets.MSetGenTree]
Props.In_1 [lemma, in Coq.MSets.MSetGenTree]
Props.isok [definition, in Coq.MSets.MSetGenTree]
Props.IsOk [definition, in Coq.MSets.MSetGenTree]
Props.isok_Ok [instance, in Coq.MSets.MSetGenTree]
Props.isok_iff [lemma, in Coq.MSets.MSetGenTree]
Props.IsRoot [constructor, in Coq.MSets.MSetGenTree]
Props.is_empty_spec [lemma, in Coq.MSets.MSetGenTree]
Props.L [module, in Coq.MSets.MSetGenTree]
Props.lt [definition, in Coq.MSets.MSetGenTree]
Props.ltb_tree_iff [lemma, in Coq.MSets.MSetGenTree]
Props.ltb_tree [definition, in Coq.MSets.MSetGenTree]
Props.lt_compat [instance, in Coq.MSets.MSetGenTree]
Props.lt_strorder [instance, in Coq.MSets.MSetGenTree]
Props.lt_tree_compat [instance, in Coq.MSets.MSetGenTree]
Props.lt_tree_trans [lemma, in Coq.MSets.MSetGenTree]
Props.lt_tree_not_in [lemma, in Coq.MSets.MSetGenTree]
Props.lt_tree_node [lemma, in Coq.MSets.MSetGenTree]
Props.lt_leaf [lemma, in Coq.MSets.MSetGenTree]
Props.lt_tree [definition, in Coq.MSets.MSetGenTree]
Props.maxdepth_log_cardinal [lemma, in Coq.MSets.MSetGenTree]
Props.maxdepth_cardinal [lemma, in Coq.MSets.MSetGenTree]
Props.max_elt_spec3 [lemma, in Coq.MSets.MSetGenTree]
Props.max_elt_spec2 [lemma, in Coq.MSets.MSetGenTree]
Props.max_elt_spec1 [lemma, in Coq.MSets.MSetGenTree]
Props.mem_spec [lemma, in Coq.MSets.MSetGenTree]
Props.mindepth_log_cardinal [lemma, in Coq.MSets.MSetGenTree]
Props.mindepth_cardinal [lemma, in Coq.MSets.MSetGenTree]
Props.mindepth_maxdepth [lemma, in Coq.MSets.MSetGenTree]
Props.min_elt_spec3 [lemma, in Coq.MSets.MSetGenTree]
Props.min_elt_spec2 [lemma, in Coq.MSets.MSetGenTree]
Props.min_elt_spec1 [lemma, in Coq.MSets.MSetGenTree]
Props.MX [module, in Coq.MSets.MSetGenTree]
Props.ok [projection, in Coq.MSets.MSetGenTree]
Props.Ok [record, in Coq.MSets.MSetGenTree]
Props.ok [constructor, in Coq.MSets.MSetGenTree]
Props.Ok [inductive, in Coq.MSets.MSetGenTree]
Props.rev_elements_rev [lemma, in Coq.MSets.MSetGenTree]
Props.rev_elements_node [lemma, in Coq.MSets.MSetGenTree]
Props.rev_elements_app [lemma, in Coq.MSets.MSetGenTree]
Props.sorted_app_inv [lemma, in Coq.MSets.MSetGenTree]
Props.Subset [definition, in Coq.MSets.MSetGenTree]
Props.subsetl_spec [lemma, in Coq.MSets.MSetGenTree]
Props.subsetr_spec [lemma, in Coq.MSets.MSetGenTree]
Props.subset_spec [lemma, in Coq.MSets.MSetGenTree]
Props.tree_ind [definition, in Coq.MSets.MSetGenTree]
prop_ext [lemma, in Coq.Logic.Diaconescu]
prop_ext_retract_A_A_imp_A [lemma, 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_degen_em [lemma, in Coq.Logic.ClassicalFacts]
prop_degen_ext [lemma, in Coq.Logic.ClassicalFacts]
prop_extensionality [definition, in Coq.Logic.ClassicalFacts]
prop_degeneracy [definition, in Coq.Logic.ClassicalFacts]
prop_on2 [definition, in Coq.ssr.ssrbool]
prop_on1 [definition, in Coq.ssr.ssrbool]
prop_in3 [definition, in Coq.ssr.ssrbool]
prop_in21 [definition, in Coq.ssr.ssrbool]
prop_in12 [definition, in Coq.ssr.ssrbool]
prop_in111 [definition, in Coq.ssr.ssrbool]
prop_in2 [definition, in Coq.ssr.ssrbool]
prop_in11 [definition, in Coq.ssr.ssrbool]
prop_in1 [definition, in Coq.ssr.ssrbool]
prop_for [definition, in Coq.ssr.ssrbool]
prop_congr [lemma, in Coq.ssr.ssrbool]
prop_eps [lemma, in Coq.Reals.Rlimit]
protected_to_nat [definition, in Coq.setoid_ring.ArithRing]
protect_term [definition, in Coq.ssr.ssreflect]
ProvablePropositionExtensionality [abbreviation, in Coq.Logic.PropExtensionalityFacts]
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_var2 [lemma, in Coq.Reals.Ranalysis4]
pr_nu_var [lemma, in Coq.Reals.Ranalysis4]
pr_nu_var2_interv [lemma, in Coq.Reals.Ranalysis5]
Psatz [inductive, in Coq.micromega.RingMicromega]
Psatz [library]
PsatzAdd [constructor, in Coq.micromega.RingMicromega]
PsatzC [constructor, in Coq.micromega.RingMicromega]
PsatzIn [constructor, in Coq.micromega.RingMicromega]
PsatzMulC [constructor, in Coq.micromega.RingMicromega]
PsatzMulE [constructor, in Coq.micromega.RingMicromega]
PsatzSquare [constructor, in Coq.micromega.RingMicromega]
PsatzZ [constructor, in Coq.micromega.RingMicromega]
Pser [definition, in Coq.Reals.Rseries]
PSeries_reg [library]
Pshiftl_nat_plus [lemma, in Coq.NArith.Ndigits]
Pshiftl_nat_N [lemma, in Coq.NArith.Ndigits]
Pshiftl_nat_S [lemma, in Coq.NArith.Ndigits]
Pshiftl_nat_0 [lemma, in Coq.NArith.Ndigits]
Psize [abbreviation, in Coq.PArith.BinPos]
Psize_log_inf [lemma, in Coq.ZArith.Zlogarithm]
Psize_pos_le [abbreviation, in Coq.PArith.BinPos]
Psize_pos_gt [abbreviation, in Coq.PArith.BinPos]
Psize_monotone [abbreviation, in Coq.PArith.BinPos]
Psize_pos [abbreviation, in Coq.PArith.BinPos]
PSome [constructor, in Coq.rtauto.Bintree]
psos_r1 [lemma, in Coq.nsatz.Nsatz]
psos_r1b [lemma, in Coq.nsatz.Nsatz]
Psquare [definition, in Coq.micromega.EnvRing]
Psquare [definition, in Coq.setoid_ring.Ncring_polynom]
Psquare [abbreviation, in Coq.ZArith.Zpow_facts]
Psquare_ok [lemma, in Coq.micromega.EnvRing]
Psquare_xI [abbreviation, in Coq.PArith.BinPos]
Psquare_xO [abbreviation, in Coq.PArith.BinPos]
Psquare_ok [lemma, in Coq.setoid_ring.Ncring_polynom]
Psquare_correct [abbreviation, in Coq.ZArith.Zpow_facts]
Psub [definition, in Coq.micromega.EnvRing]
psub [definition, in Coq.micromega.ZMicromega]
psub [definition, in Coq.micromega.RingMicromega]
Psub [definition, in Coq.setoid_ring.Ncring_polynom]
Psub [definition, in Coq.setoid_ring.Ring_polynom]
PsubC [definition, in Coq.micromega.EnvRing]
psubC [definition, in Coq.micromega.RingMicromega]
PsubC [definition, in Coq.setoid_ring.Ring_polynom]
PsubC_ok [lemma, in Coq.micromega.EnvRing]
PsubC_ok [definition, in Coq.micromega.RingMicromega]
PsubC_ok [lemma, in Coq.setoid_ring.Ring_polynom]
PsubI [definition, in Coq.micromega.EnvRing]
PsubI [definition, in Coq.setoid_ring.Ring_polynom]
PSubstL [definition, in Coq.micromega.EnvRing]
PSubstL [definition, in Coq.setoid_ring.Ring_polynom]
PSubstL_ok [lemma, in Coq.micromega.EnvRing]
PSubstL_ok [lemma, in Coq.setoid_ring.Ring_polynom]
PSubstL1 [definition, in Coq.micromega.EnvRing]
PSubstL1 [definition, in Coq.setoid_ring.Ring_polynom]
PSubstL1_ok [lemma, in Coq.micromega.EnvRing]
PSubstL1_ok [lemma, in Coq.setoid_ring.Ring_polynom]
PsubX [definition, in Coq.micromega.EnvRing]
PsubX [definition, in Coq.setoid_ring.Ring_polynom]
PsubX_ok [lemma, in Coq.micromega.EnvRing]
Psub_ok [lemma, in Coq.micromega.EnvRing]
Psub_ok [lemma, in Coq.setoid_ring.Ncring_polynom]
Psub_ok [lemma, in Coq.setoid_ring.Ring_polynom]
Psub_opp [lemma, in Coq.setoid_ring.Ring_polynom]
Psucc [abbreviation, in Coq.PArith.BinPos]
Psucc_inj [abbreviation, in Coq.PArith.BinPos]
Psucc_pred [abbreviation, in Coq.PArith.BinPos]
Psucc_not_one [abbreviation, in Coq.PArith.BinPos]
Psucc_o_double_minus_one_eq_xO [abbreviation, in Coq.PArith.BinPos]
Psucc_discr [abbreviation, in Coq.PArith.BinPos]
Psucc_Gt [lemma, in Coq.rtauto.Bintree]
Psucc_S [abbreviation, in Coq.PArith.Pnat]
ps_atan_continuity_pt_1 [lemma, in Coq.Reals.Ratan]
ps_atanSeq_continuity_pt_1 [lemma, in Coq.Reals.Ratan]
ps_atan_opp [lemma, in Coq.Reals.Ratan]
ps_atan_exists_1_opp [lemma, in Coq.Reals.Ratan]
ps_atan0_0 [lemma, in Coq.Reals.Ratan]
ps_atan [definition, in Coq.Reals.Ratan]
ps_atan_exists_1 [definition, in Coq.Reals.Ratan]
ps_atan_exists_01 [definition, in Coq.Reals.Ratan]
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]
Ptestbit_Pbit [lemma, in Coq.NArith.Ndigits]
push [definition, in Coq.rtauto.Bintree]
push_not_empty [lemma, in Coq.rtauto.Bintree]
PX [constructor, in Coq.micromega.EnvRing]
PX [constructor, in Coq.setoid_ring.Ncring_polynom]
PX [constructor, in Coq.setoid_ring.Ring_polynom]
Pxor [abbreviation, in Coq.NArith.Ndigits]
Pxor_semantics [lemma, in Coq.NArith.Ndigits]
PX_ext [instance, in Coq.setoid_ring.Ring_polynom]
P_nth [inductive, in Coq.Arith.Between]
P_eventually_implies_acc_ex [lemma, in Coq.Logic.ConstructiveEpsilon]
P_eventually_implies_acc [lemma, in Coq.Logic.ConstructiveEpsilon]
P_implies_acc [lemma, in Coq.Logic.ConstructiveEpsilon]
P_of_succ_nat [abbreviation, in Coq.PArith.BinPos]
P_Rmin [lemma, in Coq.Reals.Rpower]
P_of_succ_nat_o_nat_of_P_eq_succ [abbreviation, in Coq.PArith.Pnat]
P_of_succ_nat_of_P [abbreviation, in Coq.PArith.Pnat]
P' [definition, in Coq.Logic.ConstructiveEpsilon]
P'_decidable [lemma, in Coq.Logic.ConstructiveEpsilon]
P0 [definition, in Coq.micromega.EnvRing]
P0 [definition, in Coq.setoid_ring.Ncring_polynom]
P0 [definition, in Coq.setoid_ring.Ring_polynom]
P0Z [definition, in Coq.nsatz.Nsatz]
P0Z_correct [lemma, in Coq.nsatz.Nsatz]
P1 [definition, in Coq.micromega.EnvRing]
P1 [definition, in Coq.setoid_ring.Ncring_polynom]
P1 [definition, in Coq.setoid_ring.Ring_polynom]
P2Bv [definition, in Coq.NArith.Ndigits]
P2Bv_sized [definition, in Coq.NArith.Ndigits]
p2i [definition, in Coq.Numbers.Cyclic.Int31.Int31]
p2ibis [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]
p2ibis_spec [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
p2ibis_bounded [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]


Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (21801 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (910 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (729 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1464 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (494 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (10179 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (676 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (537 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (374 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (287 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (457 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (616 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1332 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (3609 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (137 entries)