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 (21445 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 (889 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 (714 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 (482 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 (10031 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 (663 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 (285 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 (1328 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 (3468 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 (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_succ_succ [in Coq.PArith.BinPos]
Pcompare_p_Sp [in Coq.PArith.BinPos]
Pcompare_spec [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]
Pdiv2 [in Coq.PArith.BinPos]
Pdiv2_up [in Coq.PArith.BinPos]
Pdouble_minus_one_o_succ_eq_xI [in Coq.PArith.BinPos]
Pdouble_minus_two [in Coq.PArith.BinPos]
Pdouble_mask [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 [in Coq.PArith.BinPos]
Peqb [in Coq.NArith.Ndec]
Peqb_eq [in Coq.PArith.BinPos]
Peqb_refl [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]
Pge [in Coq.PArith.BinPos]
Pge_ge [in Coq.PArith.Pnat]
Pgt [in Coq.PArith.BinPos]
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]
Piter_op_succ [in Coq.PArith.BinPos]
Piter_op [in Coq.PArith.BinPos]
Ple [in Coq.PArith.BinPos]
Ple_succ_l [in Coq.PArith.BinPos]
Ple_trans [in Coq.PArith.BinPos]
Ple_lt_trans [in Coq.PArith.BinPos]
Ple_refl [in Coq.PArith.BinPos]
Ple_lteq [in Coq.PArith.BinPos]
Ple_le [in Coq.PArith.Pnat]
Plt [in Coq.PArith.BinPos]
Plt_not_plus_l [in Coq.PArith.BinPos]
Plt_plus_r [in Coq.PArith.BinPos]
Plt_succ_r [in Coq.PArith.BinPos]
Plt_le_trans [in Coq.PArith.BinPos]
Plt_ind [in Coq.PArith.BinPos]
Plt_trans [in Coq.PArith.BinPos]
Plt_irrefl [in Coq.PArith.BinPos]
Plt_lt_succ [in Coq.PArith.BinPos]
Plt_1_succ [in Coq.PArith.BinPos]
Plt_1 [in Coq.PArith.BinPos]
Plt_lt [in Coq.PArith.Pnat]
plus [in Coq.Init.Peano]
plus_lt_is_lt [in Coq.Reals.RIneq]
plus_le_is_le [in Coq.Reals.RIneq]
plus_permute_2_in_4 [in Coq.Arith.Plus]
plus_permute [in Coq.Arith.Plus]
plus_assoc [in Coq.Arith.Plus]
plus_comm [in Coq.Arith.Plus]
plus_0_r [in Coq.Arith.Plus]
plus_0_l [in Coq.Arith.Plus]
plus_succ_r_reverse [in Coq.Init.Peano]
plus_0_r_reverse [in Coq.Init.Peano]
Pmax [in Coq.PArith.BinPos]
Pmin [in Coq.PArith.BinPos]
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]
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.mul_eq_1 [in Coq.PArith.BinPos]
pow [in Coq.Numbers.Natural.Peano.NPeano]
Power [in Coq.Wellfounded.Lexicographic_Exponentiation]
pow_succ_r [in Coq.Numbers.Natural.Peano.NPeano]
pow_0_r [in Coq.Numbers.Natural.Peano.NPeano]
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]
Ppow [in Coq.PArith.BinPos]
Ppow_gt_1 [in Coq.PArith.BinPos]
Ppow_succ_r [in Coq.PArith.BinPos]
Ppow_1_r [in Coq.PArith.BinPos]
Ppred [in Coq.PArith.BinPos]
Ppred_mask [in Coq.PArith.BinPos]
Ppred_succ [in Coq.PArith.BinPos]
Ppred_Nsucc [in Coq.NArith.BinNat]
Ppred_N_spec [in Coq.NArith.BinNat]
Ppred_N [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_class [in Coq.ssr.ssrbool]
pred_o_P_of_succ_nat_o_nat_of_P_eq_id [in Coq.PArith.Pnat]
prodT [in Coq.Init.Datatypes]
prodT_curry [in Coq.Init.Datatypes]
prodT_uncurry [in Coq.Init.Datatypes]
prodT_ind [in Coq.Init.Datatypes]
prodT_rec [in Coq.Init.Datatypes]
prodT_rect [in Coq.Init.Datatypes]
prod_f_SO [in Coq.Reals.Rprod]
prod_neq_R0 [in Coq.Reals.RIneq]
projS1 [in Coq.Init.Specif]
projS2 [in Coq.Init.Specif]
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 [in Coq.ZArith.Zpow_facts]
Psquare_xI [in Coq.PArith.BinPos]
Psquare_xO [in Coq.PArith.BinPos]
Psquare_correct [in Coq.ZArith.Zpow_facts]
Psucc [in Coq.PArith.BinPos]
Psucc_inj [in Coq.PArith.BinPos]
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_discr [in Coq.PArith.BinPos]
Psucc_S [in Coq.PArith.Pnat]
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]



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 (21445 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 (889 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 (714 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 (482 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 (10031 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 (663 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 (285 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 (1328 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 (3468 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)