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 (25892 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 (1000 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 (809 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 (1611 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 (586 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 (11840 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 (957 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 (627 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 (307 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 (477 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 (493 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 (903 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 (1211 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 (4907 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 (164 entries)

P (abbreviation)

pairT [in Coq.Init.Datatypes]
Pbit [in Coq.NArith.Ndigits]
Pcase [in Coq.PArith.BinPos]
Pcompare [in Coq.PArith.BinPos]
Pcompare_1 [in Coq.PArith.BinPos]
Pcompare_p_Sp [in Coq.PArith.BinPos]
Pcompare_antisym [in Coq.PArith.BinPos]
Pcompare_Lt_Gt [in Coq.PArith.BinPos]
Pcompare_eq_Lt [in Coq.PArith.BinPos]
Pcompare_Gt_Lt [in Coq.PArith.BinPos]
Pcompare_eq_iff [in Coq.PArith.BinPos]
Pcompare_refl_id [in Coq.PArith.BinPos]
Pcompare_nat_compare [in Coq.PArith.Pnat]
Pdouble_minus_one_o_succ_eq_xI [in Coq.PArith.BinPos]
Pdouble_minus_two [in Coq.PArith.BinPos]
Pdouble_plus_one_mask [in Coq.PArith.BinPos]
Pdouble_minus_one [in Coq.PArith.BinPos]
PeanoOne [in Coq.PArith.BinPos]
PeanoSucc [in Coq.PArith.BinPos]
peanoView [in Coq.PArith.BinPos]
PeanoView [in Coq.PArith.BinPos]
PeanoViewUnique [in Coq.PArith.BinPos]
PeanoView_iter [in Coq.PArith.BinPos]
peanoView_xI [in Coq.PArith.BinPos]
peanoView_xO [in Coq.PArith.BinPos]
PeanoView_rec [in Coq.PArith.BinPos]
PeanoView_ind [in Coq.PArith.BinPos]
PeanoView_rect [in Coq.PArith.BinPos]
Peqb_correct [in Coq.NArith.Ndec]
permutation [in Coq.Sorting.PermutEq]
Permutation_app_swap [in Coq.Sorting.Permutation]
permut_tran [in Coq.Sorting.PermutSetoid]
permut_right [in Coq.Sorting.PermutSetoid]
PExpr [in Coq.micromega.EnvRing]
Pge_ge [in Coq.PArith.Pnat]
Pgt_gt [in Coq.PArith.Pnat]
ph [in Coq.ssr.ssrbool]
ph [in Coq.ssr.ssrbool]
phi_pos1 [in Coq.micromega.ZCoeff]
phi_pos [in Coq.micromega.ZCoeff]
Pind [in Coq.PArith.BinPos]
Ple_le [in Coq.PArith.Pnat]
Plt_not_plus_l [in Coq.PArith.BinPos]
Plt_plus_r [in Coq.PArith.BinPos]
Plt_1 [in Coq.PArith.BinPos]
Plt_lt [in Coq.PArith.Pnat]
plus [in Coq.Init.Peano]
plus_succ_r_reverse [in Coq.Init.Peano]
plus_0_r_reverse [in Coq.Init.Peano]
plus_lt_is_lt [in Coq.Reals.RIneq]
plus_le_is_le [in Coq.Reals.RIneq]
Pminus [in Coq.PArith.BinPos]
Pminus_Eq [in Coq.PArith.BinPos]
Pminus_Lt [in Coq.PArith.BinPos]
Pminus_mask_Lt [in Coq.PArith.BinPos]
Pminus_minus_distr [in Coq.PArith.BinPos]
Pminus_plus_distr [in Coq.PArith.BinPos]
Pminus_xI_xI [in Coq.PArith.BinPos]
Pminus_decr [in Coq.PArith.BinPos]
Pminus_lt_mono_r [in Coq.PArith.BinPos]
Pminus_compare_mono_r [in Coq.PArith.BinPos]
Pminus_compare_mono_l [in Coq.PArith.BinPos]
Pminus_lt_mono_l [in Coq.PArith.BinPos]
Pminus_mask_diag [in Coq.PArith.BinPos]
Pminus_succ_r [in Coq.PArith.BinPos]
Pminus_mask_carry_spec [in Coq.PArith.BinPos]
Pminus_mask_succ_r [in Coq.PArith.BinPos]
Pminus_mask_carry [in Coq.PArith.BinPos]
Pminus_mask [in Coq.PArith.BinPos]
Pminus_minus [in Coq.PArith.Pnat]
Pmult [in Coq.PArith.BinPos]
Pmult_minus_distr_l [in Coq.PArith.BinPos]
Pmult_le_mono [in Coq.PArith.BinPos]
Pmult_le_mono_r [in Coq.PArith.BinPos]
Pmult_le_mono_l [in Coq.PArith.BinPos]
Pmult_lt_mono [in Coq.PArith.BinPos]
Pmult_lt_mono_r [in Coq.PArith.BinPos]
Pmult_lt_mono_l [in Coq.PArith.BinPos]
Pmult_compare_mono_r [in Coq.PArith.BinPos]
Pmult_compare_mono_l [in Coq.PArith.BinPos]
Pmult_1_inversion_l [in Coq.PArith.BinPos]
Pmult_reg_l [in Coq.PArith.BinPos]
Pmult_reg_r [in Coq.PArith.BinPos]
Pmult_xO_discr [in Coq.PArith.BinPos]
Pmult_xI_mult_xO_discr [in Coq.PArith.BinPos]
Pmult_assoc [in Coq.PArith.BinPos]
Pmult_plus_distr_r [in Coq.PArith.BinPos]
Pmult_plus_distr_l [in Coq.PArith.BinPos]
Pmult_comm [in Coq.PArith.BinPos]
Pmult_xI_permute_r [in Coq.PArith.BinPos]
Pmult_xO_permute_r [in Coq.PArith.BinPos]
Pmult_Sn_m [in Coq.PArith.BinPos]
Pmult_1_r [in Coq.PArith.BinPos]
Pmult_nat [in Coq.PArith.BinPos]
Pmult_mult [in Coq.PArith.Pnat]
Pol [in Coq.micromega.EnvRing]
Poption [in Coq.rtauto.Bintree]
positive [in Coq.PArith.BinPos]
PositiveSet.InL [in Coq.FSets.FSetPositive]
PositiveSet.InL [in Coq.MSets.MSetPositive]
PositiveSet.lex [in Coq.FSets.FSetPositive]
PositiveSet.lex [in Coq.MSets.MSetPositive]
positive_eq_dec [in Coq.PArith.BinPos]
positive_mask_rec [in Coq.PArith.BinPos]
positive_mask_ind [in Coq.PArith.BinPos]
positive_mask_rect [in Coq.PArith.BinPos]
positive_mask [in Coq.PArith.BinPos]
positive_ind [in Coq.PArith.BinPos]
positive_rec [in Coq.PArith.BinPos]
positive_rect [in Coq.PArith.BinPos]
pos_mod_int [in Coq.Numbers.Cyclic.Int63.Cyclic63]
Pos.mul_eq_1 [in Coq.PArith.BinPos]
Pos.sixteen [in Coq.PArith.BinPosDef]
Pos.ten [in Coq.PArith.BinPosDef]
Power [in Coq.Wellfounded.Lexicographic_Exponentiation]
powerRZ_mult_distr [in Coq.Reals.Rfunctions]
powerRZ_neg [in Coq.Reals.Rfunctions]
powerRZ_inv [in Coq.Reals.Rfunctions]
Pplus [in Coq.PArith.BinPos]
Pplus_minus_assoc [in Coq.PArith.BinPos]
Pplus_minus_eq [in Coq.PArith.BinPos]
Pplus_le_mono [in Coq.PArith.BinPos]
Pplus_le_mono_r [in Coq.PArith.BinPos]
Pplus_le_mono_l [in Coq.PArith.BinPos]
Pplus_lt_mono [in Coq.PArith.BinPos]
Pplus_lt_mono_r [in Coq.PArith.BinPos]
Pplus_lt_mono_l [in Coq.PArith.BinPos]
Pplus_compare_mono_r [in Coq.PArith.BinPos]
Pplus_compare_mono_l [in Coq.PArith.BinPos]
Pplus_diag [in Coq.PArith.BinPos]
Pplus_xO_double_minus_one [in Coq.PArith.BinPos]
Pplus_xI_double_minus_one [in Coq.PArith.BinPos]
Pplus_xO [in Coq.PArith.BinPos]
Pplus_assoc [in Coq.PArith.BinPos]
Pplus_carry_reg_l [in Coq.PArith.BinPos]
Pplus_carry_reg_r [in Coq.PArith.BinPos]
Pplus_reg_l [in Coq.PArith.BinPos]
Pplus_reg_r [in Coq.PArith.BinPos]
Pplus_carry_plus [in Coq.PArith.BinPos]
Pplus_no_neutral [in Coq.PArith.BinPos]
Pplus_succ_permute_l [in Coq.PArith.BinPos]
Pplus_succ_permute_r [in Coq.PArith.BinPos]
Pplus_comm [in Coq.PArith.BinPos]
Pplus_carry_spec [in Coq.PArith.BinPos]
Pplus_carry [in Coq.PArith.BinPos]
Pplus_plus [in Coq.PArith.Pnat]
Ppred_Nsucc [in Coq.NArith.BinNat]
Ppred_N_spec [in Coq.NArith.BinNat]
Prec [in Coq.PArith.BinPos]
Prect [in Coq.PArith.BinPos]
Prect_base [in Coq.PArith.BinPos]
Prect_succ [in Coq.PArith.BinPos]
pred [in Coq.Init.Peano]
predicate [in Coq.Classes.RelationClasses]
PredicateExtensionality [in Coq.Logic.PropExtensionalityFacts]
pred_o_P_of_succ_nat_o_nat_of_P_eq_id [in Coq.PArith.Pnat]
pred_of_simpl [in Coq.ssr.ssrbool]
prodT [in Coq.Init.Datatypes]
prodT_ind [in Coq.Init.Datatypes]
prodT_rec [in Coq.Init.Datatypes]
prodT_rect [in Coq.Init.Datatypes]
prod_length [in Coq.Lists.List]
prod_f_SO [in Coq.Reals.Rprod]
prod_neq_R0 [in Coq.Reals.RIneq]
PropositionalExtensionality [in Coq.Logic.PropExtensionalityFacts]
PropositionalFunctionalExtensionality [in Coq.Logic.PropExtensionalityFacts]
ProvablePropositionExtensionality [in Coq.Logic.PropExtensionalityFacts]
Psize [in Coq.PArith.BinPos]
Psize_pos_le [in Coq.PArith.BinPos]
Psize_pos_gt [in Coq.PArith.BinPos]
Psize_monotone [in Coq.PArith.BinPos]
Psize_pos [in Coq.PArith.BinPos]
Psquare_correct [in Coq.ZArith.Zpow_facts]
Psucc_pred [in Coq.PArith.BinPos]
Psucc_not_one [in Coq.PArith.BinPos]
Psucc_o_double_minus_one_eq_xO [in Coq.PArith.BinPos]
Psucc_S [in Coq.PArith.Pnat]
push [in Coq.micromega.Tauto]
Pxor [in Coq.NArith.Ndigits]
P_of_succ_nat [in Coq.PArith.BinPos]
P_of_succ_nat_o_nat_of_P_eq_succ [in Coq.PArith.Pnat]
P_of_succ_nat_of_P [in Coq.PArith.Pnat]
P_Rmin [in Coq.Reals.Rpower]



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 (25892 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 (1000 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 (809 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 (1611 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 (586 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 (11840 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 (957 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 (627 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 (307 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 (477 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 (493 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 (903 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 (1211 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 (4907 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 (164 entries)