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 (18816 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 (644 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 (708 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 (1456 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 (407 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 (8932 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 (422 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 (699 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 (209 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 (203 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 (550 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 (338 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 (1235 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 (2946 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 (67 entries)

P

pair [constructor, in pair]
PairDecidableType [module, in PairDecidableType]
PairDecidableType [module, in PairDecidableType]
PairDecidableType.eq [definition, in eq]
PairDecidableType.eq [definition, in eq]
PairDecidableType.eq_refl [lemma, in eq_refl]
PairDecidableType.eq_sym [lemma, in eq_sym]
PairDecidableType.eq_trans [lemma, in eq_trans]
PairDecidableType.eq_dec [definition, in eq_dec]
PairDecidableType.eq_dec [definition, in eq_dec]
PairDecidableType.eq_equiv [instance, in eq_equiv]
PairDecidableType.t [definition, in t]
PairDecidableType.t [definition, in t]
PairOrderedType [module, in PairOrderedType]
PairOrderedType [module, in PairOrderedType]
PairOrderedType.compare [definition, in compare]
PairOrderedType.compare [definition, in compare]
PairOrderedType.compare_spec [lemma, in compare_spec]
PairOrderedType.eq [definition, in eq]
PairOrderedType.eq_refl [lemma, in eq_refl]
PairOrderedType.eq_sym [lemma, in eq_sym]
PairOrderedType.eq_trans [lemma, in eq_trans]
PairOrderedType.eq_dec [definition, in eq_dec]
PairOrderedType.lt [definition, in lt]
PairOrderedType.lt [definition, in lt]
PairOrderedType.lt_compat [instance, in lt_compat]
PairOrderedType.lt_strorder [instance, in lt_strorder]
PairOrderedType.lt_not_eq [lemma, in lt_not_eq]
PairOrderedType.lt_trans [lemma, in lt_trans]
PairOrderedType.MO1 [module, in PairOrderedType.MO1]
PairOrderedType.MO2 [module, in PairOrderedType.MO2]
PairOrderedType.t [definition, in t]
pairT [abbreviation, in pairT]
PairUsualDecidableType [module, in PairUsualDecidableType]
PairUsualDecidableType [module, in PairUsualDecidableType]
PairUsualDecidableType.eq [definition, in eq]
PairUsualDecidableType.eq [definition, in eq]
PairUsualDecidableType.eq_refl [definition, in eq_refl]
PairUsualDecidableType.eq_sym [definition, in eq_sym]
PairUsualDecidableType.eq_trans [definition, in eq_trans]
PairUsualDecidableType.eq_dec [definition, in eq_dec]
PairUsualDecidableType.eq_dec [definition, in eq_dec]
PairUsualDecidableType.eq_equiv [instance, in eq_equiv]
PairUsualDecidableType.t [definition, in t]
PairUsualDecidableType.t [definition, in t]
pair_compat [instance, in pair_compat]
Pand_semantics [lemma, in Pand_semantics]
paradox [lemma, in paradox]
Paradox [section, in Paradox]
Paradox.B [variable, in B]
Paradox.bool [variable, in bool]
Paradox.b2p [variable, in b2p]
Paradox.p2b [variable, in p2b]
Paradox.p2p1 [variable, in p2p1]
Paradox.p2p2 [variable, in p2p2]
Params [record, in Params]
PArith [library]
PartialApplication [record, in PartialApplication]
PartialOrder [record, in PartialOrder]
PartialOrder [inductive, in PartialOrder]
PartialOrder_inverse [lemma, in PartialOrder_inverse]
PartialOrder_proper [instance, in PartialOrder_proper]
PartialOrder_StrictOrder [lemma, in PartialOrder_StrictOrder]
PartialSetoid [record, in PartialSetoid]
Partial_orders.p [variable, in p]
Partial_order_facts.U [variable, in U]
Partial_orders.U [variable, in U]
Partial_order_facts [section, in Partial_order_facts]
Partial_order_facts.D [variable, in D]
partial_order_equivalence [projection, in partial_order_equivalence]
partial_order_equivalence [constructor, in partial_order_equivalence]
Partial_orders [section, in Partial_orders]
partial_order_antisym [instance, in partial_order_antisym]
Partial_Order [library]
partition [definition, in partition]
PartSum [library]
pascal [lemma, in pascal]
pascal_step2 [lemma, in pascal_step2]
pascal_step3 [lemma, in pascal_step3]
pascal_step1 [lemma, in pascal_step1]
Pbit [abbreviation, in Pbit]
Pbit_faithful [lemma, in Pbit_faithful]
Pbit_faithful_0 [lemma, in Pbit_faithful_0]
Pbit_Ptestbit [lemma, in Pbit_Ptestbit]
Pcase [abbreviation, in Pcase]
Pcompare [abbreviation, in Pcompare]
Pcompare [definition, in Pcompare]
Pcompare_Eq_eq [lemma, in Pcompare_Eq_eq]
Pcompare_1 [abbreviation, in Pcompare_1]
Pcompare_Gt_Lt [abbreviation, in Pcompare_Gt_Lt]
Pcompare_eq_Lt [abbreviation, in Pcompare_eq_Lt]
Pcompare_succ_succ [abbreviation, in Pcompare_succ_succ]
Pcompare_Lt_Gt [abbreviation, in Pcompare_Lt_Gt]
Pcompare_antisym [abbreviation, in Pcompare_antisym]
Pcompare_spec [abbreviation, in Pcompare_spec]
Pcompare_eq_iff [abbreviation, in Pcompare_eq_iff]
Pcompare_eq_Gt [lemma, in Pcompare_eq_Gt]
Pcompare_p_Sp [abbreviation, in Pcompare_p_Sp]
Pcompare_refl [lemma, in Pcompare_refl]
Pcompare_nat_compare [abbreviation, in Pcompare_nat_compare]
Pcompare_refl_id [abbreviation, in Pcompare_refl_id]
Pcompare_Peqb [lemma, in Pcompare_Peqb]
Pdiff_semantics [lemma, in Pdiff_semantics]
Pdiv [definition, in Pdiv]
Pdiv_eucl [definition, in Pdiv_eucl]
Pdiv_eucl_remainder [lemma, in Pdiv_eucl_remainder]
Pdiv_le [lemma, in Pdiv_le]
Pdiv_eucl_correct [definition, in Pdiv_eucl_correct]
Pdiv2 [lemma, in Pdiv2]
Pdiv2 [abbreviation, in Pdiv2]
Pdiv2_up [abbreviation, in Pdiv2_up]
Pdouble_minus_two [abbreviation, in Pdouble_minus_two]
Pdouble_plus_one_mask [abbreviation, in Pdouble_plus_one_mask]
Pdouble_mask [abbreviation, in Pdouble_mask]
Pdouble_minus_one [abbreviation, in Pdouble_minus_one]
Pdouble_minus_one_o_succ_eq_xI [abbreviation, in Pdouble_minus_one_o_succ_eq_xI]
Peano [library]
PeanoOne [abbreviation, in PeanoOne]
PeanoSucc [abbreviation, in PeanoSucc]
peanoView [abbreviation, in peanoView]
PeanoView [abbreviation, in PeanoView]
PeanoViewUnique [abbreviation, in PeanoViewUnique]
PeanoView_rec [abbreviation, in PeanoView_rec]
PeanoView_rect [abbreviation, in PeanoView_rect]
PeanoView_iter [abbreviation, in PeanoView_iter]
PeanoView_ind [abbreviation, in PeanoView_ind]
peanoView_xI [abbreviation, in peanoView_xI]
peanoView_xO [abbreviation, in peanoView_xO]
Peano_dec [library]
Peirce [lemma, in Peirce]
Peqb [abbreviation, in Peqb]
Peqb [abbreviation, in Peqb]
Peqb_correct [abbreviation, in Peqb_correct]
Peqb_refl [abbreviation, in Peqb_refl]
Peqb_eq [abbreviation, in Peqb_eq]
Peqb_complete [lemma, in Peqb_complete]
Peqb_Pcompare [lemma, in Peqb_Pcompare]
Peqb_true_eq [lemma, in Peqb_true_eq]
pequiv [projection, in pequiv]
pequiv [definition, in pequiv]
pequiv_prf [projection, in pequiv_prf]
PER [record, in PER]
PER [record, in PER]
PER [inductive, in PER]
Perm [section, in Perm]
permA_skip [constructor, in permA_skip]
permA_swap [constructor, in permA_swap]
permA_trans [constructor, in permA_trans]
permA_nil [constructor, in permA_nil]
Permut [section, in Permut]
Permut [library]
permutation [abbreviation, in permutation]
permutation [definition, in permutation]
Permutation [inductive, in Permutation]
Permutation [section, in Permutation]
Permutation [section, in Permutation]
Permutation [library]
PermutationA [inductive, in PermutationA]
PermutationA_app_comm [lemma, in PermutationA_app_comm]
PermutationA_cons [instance, in PermutationA_cons]
PermutationA_app_tail [lemma, in PermutationA_app_tail]
PermutationA_cons_append [lemma, in PermutationA_cons_append]
PermutationA_app_head [lemma, in PermutationA_app_head]
PermutationA_cons_app [lemma, in PermutationA_cons_app]
PermutationA_middle [lemma, in PermutationA_middle]
PermutationA_equivlistA [lemma, in PermutationA_equivlistA]
PermutationA_app [instance, in PermutationA_app]
Permutation_length_1_inv [lemma, in Permutation_length_1_inv]
Permutation_refl [lemma, in Permutation_refl]
Permutation_middle [lemma, in Permutation_middle]
Permutation_length_2 [lemma, in Permutation_length_2]
Permutation_app_inv_r [lemma, in Permutation_app_inv_r]
Permutation_in [lemma, in Permutation_in]
Permutation_nil [lemma, in Permutation_nil]
Permutation_app_inv [lemma, in Permutation_app_inv]
Permutation_map.B [variable, in B]
Permutation_rev [lemma, in Permutation_rev]
Permutation_cons_inv [lemma, in Permutation_cons_inv]
Permutation_ind_bis [lemma, in Permutation_ind_bis]
Permutation_app_tail [lemma, in Permutation_app_tail]
Permutation_length_2_inv [lemma, in Permutation_length_2_inv]
Permutation_map.f [variable, in f]
Permutation_length_1 [lemma, in Permutation_length_1]
permutation_map [lemma, in permutation_map]
Permutation_cons_app_inv [lemma, in Permutation_cons_app_inv]
Permutation_properties [section, in Permutation_properties]
Permutation_app [lemma, in Permutation_app]
Permutation_Equivalence [instance, in Permutation_Equivalence]
Permutation_app_comm [lemma, in Permutation_app_comm]
Permutation_length [lemma, in Permutation_length]
Permutation_app_inv_l [lemma, in Permutation_app_inv_l]
Permutation_cons_app [lemma, in Permutation_cons_app]
permutation_Permutation [lemma, in permutation_Permutation]
permutation_Permutation [lemma, in permutation_Permutation]
Permutation_nil_cons [lemma, in Permutation_nil_cons]
Permutation_add_inside [lemma, in Permutation_add_inside]
Permutation_nil_app_cons [lemma, in Permutation_nil_app_cons]
Permutation_impl_permutation [lemma, in Permutation_impl_permutation]
Permutation_map.A [variable, in A]
Permutation_properties.A [variable, in A]
Permutation_app_swap [abbreviation, in Permutation_app_swap]
Permutation_sym [lemma, in Permutation_sym]
Permutation_trans [lemma, in Permutation_trans]
Permutation_map [lemma, in Permutation_map]
Permutation_map [section, in Permutation_map]
Permutation_cons_append [lemma, in Permutation_cons_append]
Permutation_app_head [lemma, in Permutation_app_head]
Permutation.A [variable, in A]
PermutEq [library]
PermutSetoid [library]
permut_In_In [lemma, in permut_In_In]
Permut_map.eqB_dec [variable, in eqB_dec]
permut_add_cons_inside_eq [lemma, in permut_add_cons_inside_eq]
permut_eqA [lemma, in permut_eqA]
Permut_permut.eqA [variable, in eqA]
Permut_map.eqA [variable, in eqA]
Permut_permut.eqA_dec [variable, in eqA_dec]
Permut_map.eqA_dec [variable, in eqA_dec]
permut_length_1 [lemma, in permut_length_1]
permut_length_1 [lemma, in permut_length_1]
Permut_map.eqB_trans [variable, in eqB_trans]
permut_tran [abbreviation, in permut_tran]
Permut_map.B [variable, in B]
permut_nil [lemma, in permut_nil]
permut_nil [lemma, in permut_nil]
permut_sym [lemma, in permut_sym]
permut_remove_hd [lemma, in permut_remove_hd]
permut_sym_app [lemma, in permut_sym_app]
permut_refl [lemma, in permut_refl]
permut_map [lemma, in permut_map]
permut_length_2 [lemma, in permut_length_2]
permut_length_2 [lemma, in permut_length_2]
permut_app_inv2 [lemma, in permut_app_inv2]
Permut_map [section, in Permut_map]
permut_cons_In [lemma, in permut_cons_In]
permut_cons_InA [lemma, in permut_cons_InA]
permut_length [lemma, in permut_length]
permut_length [lemma, in permut_length]
permut_rev [lemma, in permut_rev]
permut_trans [lemma, in permut_trans]
Permut_map.eqB [variable, in eqB]
permut_middle [lemma, in permut_middle]
Permut_permut.eqA_equiv [variable, in eqA_equiv]
Permut_map.eqA_equiv [variable, in eqA_equiv]
permut_app_inv1 [lemma, in permut_app_inv1]
Permut_permut.A [variable, in A]
Permut_map.A [variable, in A]
permut_add_inside_eq [lemma, in permut_add_inside_eq]
permut_cons_eq [lemma, in permut_cons_eq]
permut_add_cons_inside [lemma, in permut_add_cons_inside]
permut_add_inside [lemma, in permut_add_inside]
permut_conv_inv [lemma, in permut_conv_inv]
permut_remove_hd_eq [lemma, in permut_remove_hd_eq]
Permut_permut [section, in Permut_permut]
permut_cons [lemma, in permut_cons]
permut_right [abbreviation, in permut_right]
permut_InA_InA [lemma, in permut_InA_InA]
permut_app [lemma, in permut_app]
Permut.A [variable, in A]
Permut.emptyBag [variable, in emptyBag]
Permut.eqA [variable, in eqA]
Permut.eqA_dec [variable, in eqA_dec]
Permut.eqA_equiv [variable, in eqA_equiv]
Permut.singletonBag [variable, in singletonBag]
perm_nil [constructor, in perm_nil]
perm_trans [constructor, in perm_trans]
perm_right [lemma, in perm_right]
perm_swap [constructor, in perm_swap]
perm_left [lemma, in perm_left]
perm_skip [constructor, in perm_skip]
Perm.A [variable, in A]
Perm.B [variable, in B]
Perm.eqB_dec [variable, in eqB_dec]
Perm.eq_dec [variable, in eq_dec]
PER_Transitive [projection, in PER_Transitive]
per_trans [projection, in per_trans]
per_sym [projection, in per_sym]
PER_Symmetric [projection, in PER_Symmetric]
per_partial_app_morphism [instance, in per_partial_app_morphism]
PER_morphism [instance, in PER_morphism]
Pge [abbreviation, in Pge]
Pge_ge [abbreviation, in Pge_ge]
Pgt [abbreviation, in Pgt]
Pgt_gt [abbreviation, in Pgt_gt]
phi [definition, in phi]
phibis_aux_equiv [lemma, in phibis_aux_equiv]
phibis_aux_lowerbound [lemma, in phibis_aux_lowerbound]
phibis_aux_bounded [lemma, in phibis_aux_bounded]
phibis_aux [definition, in phibis_aux]
phibis_aux_pos [lemma, in phibis_aux_pos]
phi_inv_phi_aux [lemma, in phi_inv_phi_aux]
phi_incr [lemma, in phi_incr]
phi_nz [lemma, in phi_nz]
phi_bounded [lemma, in phi_bounded]
phi_gcd [lemma, in phi_gcd]
phi_inv_phi [lemma, in phi_inv_phi]
phi_twice_firstl [lemma, in phi_twice_firstl]
phi_twice_plus_one_firstl [lemma, in phi_twice_plus_one_firstl]
phi_inv_positive_p2ibis [lemma, in phi_inv_positive_p2ibis]
phi_inv_positive [definition, in phi_inv_positive]
phi_phi_inv [lemma, in phi_phi_inv]
phi_twice [lemma, in phi_twice]
phi_inv_double_plus_one [lemma, in phi_inv_double_plus_one]
phi_inv2 [definition, in phi_inv2]
phi_lowerbound [lemma, in phi_lowerbound]
phi_sequence_prop [lemma, in phi_sequence_prop]
phi_eqn1 [lemma, in phi_eqn1]
phi_twice_plus_one [lemma, in phi_twice_plus_one]
phi_sequence [definition, in phi_sequence]
phi_phi_inv_negative [lemma, in phi_phi_inv_negative]
phi_inv [definition, in phi_inv]
phi_eqn2 [lemma, in phi_eqn2]
phi_inv_incr [lemma, in phi_inv_incr]
phi_inv_double [lemma, in phi_inv_double]
phi_phi_inv_positive [lemma, in phi_phi_inv_positive]
phi2 [definition, in phi2]
phi2_phi_inv2 [lemma, in phi2_phi_inv2]
PI [definition, in PI]
PI [module, in PI]
Pigeonhole [lemma, in Pigeonhole]
Pigeonhole_principle [lemma, in Pigeonhole_principle]
Pigeonhole_bis [lemma, in Pigeonhole_bis]
Pigeonhole_ter [lemma, in Pigeonhole_ter]
Pind [abbreviation, in Pind]
Piter_mul_acc [lemma, in Piter_mul_acc]
Piter_op_square [lemma, in Piter_op_square]
Piter_op [abbreviation, in Piter_op]
Piter_op_succ [abbreviation, in Piter_op_succ]
PI_2_3_7_ineq [lemma, in PI_2_3_7_ineq]
PI_tg [definition, in PI_tg]
PI_neq0 [lemma, in PI_neq0]
PI_ineq [lemma, in PI_ineq]
PI_RGT_0 [lemma, in PI_RGT_0]
PI_2_3_7_tg [definition, in PI_2_3_7_tg]
PI_tg_pos [lemma, in PI_tg_pos]
PI_tg_cv [lemma, in PI_tg_cv]
PI_4 [lemma, in PI_4]
PI_tg_decreasing [lemma, in PI_tg_decreasing]
PI_2_aux [definition, in PI_2_aux]
PI.proof_irrelevance [definition, in proof_irrelevance]
PI2 [definition, in PI2]
PI2_lower_bound [lemma, in PI2_lower_bound]
PI2_Rlt_PI [lemma, in PI2_Rlt_PI]
PI2_1 [lemma, in PI2_1]
pi2_int [lemma, in pi2_int]
PI2_3_2 [lemma, in PI2_3_2]
PI2_RGT_0 [lemma, in PI2_RGT_0]
PI4_RLT_PI2 [lemma, in PI4_RLT_PI2]
PI4_RGT_0 [lemma, in PI4_RGT_0]
PI6_RGT_0 [lemma, in PI6_RGT_0]
PI6_RLT_PI2 [lemma, in PI6_RLT_PI2]
plat [definition, in plat]
Ple [abbreviation, in Ple]
plength [definition, in plength]
plength_correct [lemma, in plength_correct]
plength_pred_correct [lemma, in plength_pred_correct]
Ple_lteq [abbreviation, in Ple_lteq]
Ple_refl [abbreviation, in Ple_refl]
Ple_succ_l [abbreviation, in Ple_succ_l]
Ple_lt_trans [abbreviation, in Ple_lt_trans]
Ple_le [abbreviation, in Ple_le]
Ple_trans [abbreviation, in Ple_trans]
Plt [abbreviation, in Plt]
Plt_plus_r [abbreviation, in Plt_plus_r]
Plt_succ_r [abbreviation, in Plt_succ_r]
Plt_ind [abbreviation, in Plt_ind]
Plt_not_plus_l [abbreviation, in Plt_not_plus_l]
Plt_lt [abbreviation, in Plt_lt]
Plt_1_succ [abbreviation, in Plt_1_succ]
Plt_lt_succ [abbreviation, in Plt_lt_succ]
Plt_trans [abbreviation, in Plt_trans]
Plt_le_trans [abbreviation, in Plt_le_trans]
Plt_irrefl [abbreviation, in Plt_irrefl]
Plt_1 [abbreviation, in Plt_1]
plus [definition, in plus]
Plus [library]
plusnS [definition, in plusnS]
plusn0 [definition, in plusn0]
plus_IZR [lemma, in plus_IZR]
plus_is_O [lemma, in plus_is_O]
plus_0_r [definition, in plus_0_r]
plus_gt_reg_l [lemma, in plus_gt_reg_l]
plus_le_compat [lemma, in plus_le_compat]
plus_lt_compat_l [lemma, in plus_lt_compat_l]
plus_max_distr_l [definition, in plus_max_distr_l]
plus_tail_plus [lemma, in plus_tail_plus]
plus_permute_2_in_4 [lemma, in plus_permute_2_in_4]
plus_le_compat_r [lemma, in plus_le_compat_r]
plus_lt_compat_r [lemma, in plus_lt_compat_r]
plus_max_distr_r [definition, in plus_max_distr_r]
plus_0_r_reverse [abbreviation, in plus_0_r_reverse]
plus_le_lt_compat [lemma, in plus_le_lt_compat]
plus_Snm_nSm [definition, in plus_Snm_nSm]
plus_Int_part1 [lemma, in plus_Int_part1]
plus_frac_part2 [lemma, in plus_frac_part2]
plus_n_O [lemma, in plus_n_O]
plus_gt_compat_l [lemma, in plus_gt_compat_l]
plus_le_compat_l [lemma, in plus_le_compat_l]
plus_reg_l [lemma, in plus_reg_l]
plus_lt_compat [lemma, in plus_lt_compat]
plus_is_one [definition, in plus_is_one]
plus_min_distr_l [definition, in plus_min_distr_l]
plus_lt_is_lt [abbreviation, in plus_lt_is_lt]
plus_assoc [lemma, in plus_assoc]
plus_O_n [lemma, in plus_O_n]
plus_Rsqr_gt_0 [lemma, in plus_Rsqr_gt_0]
plus_sum [lemma, in plus_sum]
plus_INR [lemma, in plus_INR]
plus_lt_le_compat [lemma, in plus_lt_le_compat]
plus_fct [definition, in plus_fct]
plus_comm [lemma, in plus_comm]
plus_IZR_NEG_POS [lemma, in plus_IZR_NEG_POS]
plus_permute [lemma, in plus_permute]
plus_minus [lemma, in plus_minus]
plus_min_distr_r [definition, in plus_min_distr_r]
plus_Int_part2 [lemma, in plus_Int_part2]
plus_le_is_le [abbreviation, in plus_le_is_le]
plus_0_l [abbreviation, in plus_0_l]
plus_Sn_m [lemma, in plus_Sn_m]
plus_assoc_reverse [lemma, in plus_assoc_reverse]
plus_lt_reg_l [lemma, in plus_lt_reg_l]
plus_n_Sm [lemma, in plus_n_Sm]
plus_frac_part1 [lemma, in plus_frac_part1]
plus_le_reg_l [lemma, in plus_le_reg_l]
plus_succ_r_reverse [abbreviation, in plus_succ_r_reverse]
Pmax [abbreviation, in Pmax]
Pmin [abbreviation, in Pmin]
Pminus [abbreviation, in Pminus]
Pminus_mask [abbreviation, in Pminus_mask]
Pminus_decr [abbreviation, in Pminus_decr]
Pminus_compare_mono_r [abbreviation, in Pminus_compare_mono_r]
Pminus_Eq [abbreviation, in Pminus_Eq]
Pminus_mask_carry [abbreviation, in Pminus_mask_carry]
Pminus_mask_diag [abbreviation, in Pminus_mask_diag]
Pminus_lt_mono_l [abbreviation, in Pminus_lt_mono_l]
Pminus_minus [abbreviation, in Pminus_minus]
Pminus_xI_xI [abbreviation, in Pminus_xI_xI]
Pminus_mask_Gt [lemma, in Pminus_mask_Gt]
Pminus_succ_r [abbreviation, in Pminus_succ_r]
Pminus_minus_distr [abbreviation, in Pminus_minus_distr]
Pminus_Lt [abbreviation, in Pminus_Lt]
Pminus_lt_mono_r [abbreviation, in Pminus_lt_mono_r]
Pminus_compare_mono_l [abbreviation, in Pminus_compare_mono_l]
Pminus_plus_distr [abbreviation, in Pminus_plus_distr]
Pminus_mask_succ_r [abbreviation, in Pminus_mask_succ_r]
Pminus_mask_Lt [abbreviation, in Pminus_mask_Lt]
Pminus_mask_carry_spec [abbreviation, in Pminus_mask_carry_spec]
Pmult [abbreviation, in Pmult]
Pmult_reg_l [abbreviation, in Pmult_reg_l]
Pmult_nat_mult [lemma, in Pmult_nat_mult]
Pmult_minus_distr_l [abbreviation, in Pmult_minus_distr_l]
Pmult_reg_r [abbreviation, in Pmult_reg_r]
Pmult_compare_mono_l [abbreviation, in Pmult_compare_mono_l]
Pmult_le_mono_r [abbreviation, in Pmult_le_mono_r]
Pmult_plus_distr_l [abbreviation, in Pmult_plus_distr_l]
Pmult_le_mono [abbreviation, in Pmult_le_mono]
Pmult_xI_permute_r [abbreviation, in Pmult_xI_permute_r]
Pmult_plus_distr_r [abbreviation, in Pmult_plus_distr_r]
Pmult_nat_succ_morphism [lemma, in Pmult_nat_succ_morphism]
Pmult_nat_r_plus_morphism [lemma, in Pmult_nat_r_plus_morphism]
Pmult_assoc [abbreviation, in Pmult_assoc]
Pmult_nat_l_plus_morphism [lemma, in Pmult_nat_l_plus_morphism]
Pmult_compare_mono_r [abbreviation, in Pmult_compare_mono_r]
Pmult_nat [abbreviation, in Pmult_nat]
Pmult_nat_plus_carry_morphism [lemma, in Pmult_nat_plus_carry_morphism]
Pmult_lt_mono_r [abbreviation, in Pmult_lt_mono_r]
Pmult_comm [abbreviation, in Pmult_comm]
Pmult_xO_permute_r [abbreviation, in Pmult_xO_permute_r]
Pmult_1_r [abbreviation, in Pmult_1_r]
Pmult_xI_mult_xO_discr [abbreviation, in Pmult_xI_mult_xO_discr]
Pmult_lt_mono [abbreviation, in Pmult_lt_mono]
Pmult_1_inversion_l [abbreviation, in Pmult_1_inversion_l]
Pmult_xO_discr [abbreviation, in Pmult_xO_discr]
Pmult_mult [abbreviation, in Pmult_mult]
Pmult_le_mono_l [abbreviation, in Pmult_le_mono_l]
Pmult_Sn_m [abbreviation, in Pmult_Sn_m]
Pmult_lt_mono_l [abbreviation, in Pmult_lt_mono_l]
Pnat [library]
PO [record, in PO]
pointwise_relation [definition, in pointwise_relation]
pointwise_equivalence [instance, in pointwise_equivalence]
pointwise_subrelation [instance, in pointwise_subrelation]
pointwise_pointwise [lemma, in pointwise_pointwise]
pointwise_lifting [definition, in pointwise_lifting]
pointwise_extension [definition, in pointwise_extension]
point_adherent [definition, in point_adherent]
poly [lemma, in poly]
POrderedType [library]
Por_semantics [lemma, in Por_semantics]
Pos [module, in Pos]
Pos [module, in Pos]
pos [projection, in pos]
positive [inductive, in positive]
positive [abbreviation, in positive]
PositiveMap [module, in PositiveMap]
PositiveMapAdditionalFacts [module, in PositiveMapAdditionalFacts]
PositiveMapAdditionalFacts.gsident [lemma, in gsident]
PositiveMapAdditionalFacts.gsspec [lemma, in gsspec]
PositiveMapAdditionalFacts.map2_commut [lemma, in map2_commut]
PositiveMapAdditionalFacts.xmap2_lr [lemma, in xmap2_lr]
PositiveMap.A [section, in A]
PositiveMap.add [definition, in add]
PositiveMap.add_1 [lemma, in add_1]
PositiveMap.add_2 [lemma, in add_2]
PositiveMap.add_3 [lemma, in add_3]
PositiveMap.A.A [variable, in A]
PositiveMap.A.B [variable, in B]
PositiveMap.A.CompcertSpec [section, in CompcertSpec]
PositiveMap.A.FMapSpec [section, in FMapSpec]
PositiveMap.A.FMapSpec.e [variable, in e]
PositiveMap.A.FMapSpec.e' [variable, in e']
PositiveMap.A.FMapSpec.m [variable, in m]
PositiveMap.A.FMapSpec.m' [variable, in m']
PositiveMap.A.FMapSpec.m'' [variable, in m'']
PositiveMap.A.FMapSpec.x [variable, in x]
PositiveMap.A.FMapSpec.y [variable, in y]
PositiveMap.A.FMapSpec.z [variable, in z]
PositiveMap.A.Mapi [section, in Mapi]
PositiveMap.A.Mapi.f [variable, in f]
PositiveMap.cardinal [definition, in cardinal]
PositiveMap.cardinal_1 [lemma, in cardinal_1]
PositiveMap.E [module, in PositiveMap.E]
PositiveMap.elements [definition, in elements]
PositiveMap.elements_3w [lemma, in elements_3w]
PositiveMap.elements_3 [lemma, in elements_3]
PositiveMap.elements_correct [lemma, in elements_correct]
PositiveMap.elements_1 [lemma, in elements_1]
PositiveMap.elements_complete [lemma, in elements_complete]
PositiveMap.elements_2 [lemma, in elements_2]
PositiveMap.empty [definition, in empty]
PositiveMap.Empty [definition, in Empty]
PositiveMap.Empty_Node [lemma, in Empty_Node]
PositiveMap.Empty_alt [lemma, in Empty_alt]
PositiveMap.empty_1 [lemma, in empty_1]
PositiveMap.eqke_equiv [instance, in eqke_equiv]
PositiveMap.eqk_equiv [instance, in eqk_equiv]
PositiveMap.equal [definition, in equal]
PositiveMap.Equal [definition, in Equal]
PositiveMap.equal_2 [lemma, in equal_2]
PositiveMap.equal_1 [lemma, in equal_1]
PositiveMap.Equiv [definition, in Equiv]
PositiveMap.Equivb [definition, in Equivb]
PositiveMap.eq_key_elt [definition, in eq_key_elt]
PositiveMap.eq_key [definition, in eq_key]
PositiveMap.find [definition, in find]
PositiveMap.find_2 [lemma, in find_2]
PositiveMap.find_xfind_h [lemma, in find_xfind_h]
PositiveMap.find_1 [lemma, in find_1]
PositiveMap.Fold [section, in Fold]
PositiveMap.fold [definition, in fold]
PositiveMap.fold_1 [lemma, in fold_1]
PositiveMap.Fold.A [variable, in A]
PositiveMap.Fold.B [variable, in B]
PositiveMap.Fold.f [variable, in f]
PositiveMap.gempty [lemma, in gempty]
PositiveMap.gleaf [lemma, in gleaf]
PositiveMap.gmapi [lemma, in gmapi]
PositiveMap.gmap2 [lemma, in gmap2]
PositiveMap.gro [lemma, in gro]
PositiveMap.grs [lemma, in grs]
PositiveMap.gso [lemma, in gso]
PositiveMap.gss [lemma, in gss]
PositiveMap.In [definition, in In]
PositiveMap.is_empty_1 [lemma, in is_empty_1]
PositiveMap.is_empty [definition, in is_empty]
PositiveMap.is_empty_2 [lemma, in is_empty_2]
PositiveMap.key [definition, in key]
PositiveMap.Leaf [constructor, in Leaf]
PositiveMap.ltk_strorder [instance, in ltk_strorder]
PositiveMap.lt_key [definition, in lt_key]
PositiveMap.map [definition, in map]
PositiveMap.mapi [definition, in mapi]
PositiveMap.mapi_2 [lemma, in mapi_2]
PositiveMap.mapi_1 [lemma, in mapi_1]
PositiveMap.MapsTo [definition, in MapsTo]
PositiveMap.MapsTo_1 [lemma, in MapsTo_1]
PositiveMap.map_1 [lemma, in map_1]
PositiveMap.map_2 [lemma, in map_2]
PositiveMap.map2 [definition, in map2]
PositiveMap.map2 [section, in map2]
PositiveMap.map2_2 [lemma, in map2_2]
PositiveMap.map2_1 [lemma, in map2_1]
PositiveMap.map2.A [variable, in A]
PositiveMap.map2.B [variable, in B]
PositiveMap.map2.C [variable, in C]
PositiveMap.map2.f [variable, in f]
PositiveMap.ME [module, in PositiveMap.ME]
PositiveMap.mem [definition, in mem]
PositiveMap.mem_1 [lemma, in mem_1]
PositiveMap.mem_find [lemma, in mem_find]
PositiveMap.mem_2 [lemma, in mem_2]
PositiveMap.Node [constructor, in Node]
PositiveMap.remove [definition, in remove]
PositiveMap.remove_2 [lemma, in remove_2]
PositiveMap.remove_1 [lemma, in remove_1]
PositiveMap.remove_3 [lemma, in remove_3]
PositiveMap.rleaf [lemma, in rleaf]
PositiveMap.t [definition, in t]
PositiveMap.tree [inductive, in tree]
PositiveMap.tree_ind [definition, in tree_ind]
PositiveMap.xelements [definition, in xelements]
PositiveMap.xelements_oh [lemma, in xelements_oh]
PositiveMap.xelements_hi [lemma, in xelements_hi]
PositiveMap.xelements_oi [lemma, in xelements_oi]
PositiveMap.xelements_ho [lemma, in xelements_ho]
PositiveMap.xelements_oo [lemma, in xelements_oo]
PositiveMap.xelements_correct [lemma, in xelements_correct]
PositiveMap.xelements_io [lemma, in xelements_io]
PositiveMap.xelements_complete [lemma, in xelements_complete]
PositiveMap.xelements_ii [lemma, in xelements_ii]
PositiveMap.xelements_sort [lemma, in xelements_sort]
PositiveMap.xelements_bits_lt_2 [lemma, in xelements_bits_lt_2]
PositiveMap.xelements_bits_lt_1 [lemma, in xelements_bits_lt_1]
PositiveMap.xelements_ih [lemma, in xelements_ih]
PositiveMap.xfind [definition, in xfind]
PositiveMap.xfind_left [lemma, in xfind_left]
PositiveMap.xfoldi [definition, in xfoldi]
PositiveMap.xfoldi_1 [lemma, in xfoldi_1]
PositiveMap.xgmapi [lemma, in xgmapi]
PositiveMap.xgmap2_r [lemma, in xgmap2_r]
PositiveMap.xgmap2_l [lemma, in xgmap2_l]
PositiveMap.xmapi [definition, in xmapi]
PositiveMap.xmap2_l [definition, in xmap2_l]
PositiveMap.xmap2_r [definition, in xmap2_r]
PositiveMap._map2 [definition, in _map2]
PositiveNotOne [module, in PositiveNotOne]
PositiveNotOne.not_one [axiom, in not_one]
PositiveNotOne.p [axiom, in p]
PositiveOrder [module, in PositiveOrder]
PositiveOrderedTypeBits [module, in PositiveOrderedTypeBits]
PositiveOrderedTypeBits [module, in PositiveOrderedTypeBits]
PositiveOrderedTypeBits.bits_lt [definition, in bits_lt]
PositiveOrderedTypeBits.bits_lt [definition, in bits_lt]
PositiveOrderedTypeBits.bits_lt_antirefl [lemma, in bits_lt_antirefl]
PositiveOrderedTypeBits.bits_lt_antirefl [lemma, in bits_lt_antirefl]
PositiveOrderedTypeBits.bits_lt_trans [lemma, in bits_lt_trans]
PositiveOrderedTypeBits.bits_lt_trans [lemma, in bits_lt_trans]
PositiveOrderedTypeBits.compare [definition, in compare]
PositiveOrderedTypeBits.compare [definition, in compare]
PositiveOrderedTypeBits.compare_spec [lemma, in compare_spec]
PositiveOrderedTypeBits.eq [definition, in eq]
PositiveOrderedTypeBits.eqb [definition, in eqb]
PositiveOrderedTypeBits.eqb_eq [definition, in eqb_eq]
PositiveOrderedTypeBits.eq_refl [definition, in eq_refl]
PositiveOrderedTypeBits.eq_sym [definition, in eq_sym]
PositiveOrderedTypeBits.eq_trans [definition, in eq_trans]
PositiveOrderedTypeBits.eq_dec [lemma, in eq_dec]
PositiveOrderedTypeBits.lt [definition, in lt]
PositiveOrderedTypeBits.lt [definition, in lt]
PositiveOrderedTypeBits.lt_compat [instance, in lt_compat]
PositiveOrderedTypeBits.lt_strorder [instance, in lt_strorder]
PositiveOrderedTypeBits.lt_not_eq [lemma, in lt_not_eq]
PositiveOrderedTypeBits.lt_trans [lemma, in lt_trans]
PositiveOrderedTypeBits.t [definition, in t]
PositiveOrderedTypeBits.t [definition, in t]
PositiveSet [module, in PositiveSet]
PositiveSet [module, in PositiveSet]
PositiveSet.add [definition, in add]
PositiveSet.add [definition, in add]
PositiveSet.add_1 [lemma, in add_1]
PositiveSet.add_spec [lemma, in add_spec]
PositiveSet.add_spec [lemma, in add_spec]
PositiveSet.add_2 [lemma, in add_2]
PositiveSet.add_3 [lemma, in add_3]
PositiveSet.cardinal [definition, in cardinal]
PositiveSet.cardinal [definition, in cardinal]
PositiveSet.cardinal_1 [lemma, in cardinal_1]
PositiveSet.cardinal_spec [lemma, in cardinal_spec]
PositiveSet.choose [definition, in choose]
PositiveSet.choose [definition, in choose]
PositiveSet.choose_3' [lemma, in choose_3']
PositiveSet.choose_spec3' [lemma, in choose_spec3']
PositiveSet.choose_spec3 [lemma, in choose_spec3]
PositiveSet.choose_3 [lemma, in choose_3]
PositiveSet.choose_spec2 [lemma, in choose_spec2]
PositiveSet.choose_1 [lemma, in choose_1]
PositiveSet.choose_spec1 [lemma, in choose_spec1]
PositiveSet.choose_empty [lemma, in choose_empty]
PositiveSet.choose_empty [lemma, in choose_empty]
PositiveSet.choose_2 [lemma, in choose_2]
PositiveSet.compare [definition, in compare]
PositiveSet.compare [lemma, in compare]
PositiveSet.compare_bool_inv [lemma, in compare_bool_inv]
PositiveSet.compare_bool_inv [lemma, in compare_bool_inv]
PositiveSet.compare_bool_Eq [lemma, in compare_bool_Eq]
PositiveSet.compare_bool_Eq [lemma, in compare_bool_Eq]
PositiveSet.compare_eq [lemma, in compare_eq]
PositiveSet.compare_eq [lemma, in compare_eq]
PositiveSet.compare_fun [definition, in compare_fun]
PositiveSet.compare_empty_x [lemma, in compare_empty_x]
PositiveSet.compare_empty_x [lemma, in compare_empty_x]
PositiveSet.compare_spec [lemma, in compare_spec]
PositiveSet.compare_bool [definition, in compare_bool]
PositiveSet.compare_bool [definition, in compare_bool]
PositiveSet.compare_x_empty [lemma, in compare_x_empty]
PositiveSet.compare_x_empty [lemma, in compare_x_empty]
PositiveSet.compare_compat [instance, in compare_compat]
PositiveSet.compare_equal [lemma, in compare_equal]
PositiveSet.compare_equal [lemma, in compare_equal]
PositiveSet.compare_inv [lemma, in compare_inv]
PositiveSet.compare_inv [lemma, in compare_inv]
PositiveSet.compare_gt [lemma, in compare_gt]
PositiveSet.compare_gt [lemma, in compare_gt]
PositiveSet.compare_compat_1 [instance, in compare_compat_1]
PositiveSet.compare_x_Leaf [lemma, in compare_x_Leaf]
PositiveSet.compare_x_Leaf [lemma, in compare_x_Leaf]
PositiveSet.ct [inductive, in ct]
PositiveSet.ct [inductive, in ct]
PositiveSet.ct_xxx [constructor, in ct_xxx]
PositiveSet.ct_xxx [constructor, in ct_xxx]
PositiveSet.ct_lex [lemma, in ct_lex]
PositiveSet.ct_lex [lemma, in ct_lex]
PositiveSet.ct_xex [constructor, in ct_xex]
PositiveSet.ct_xex [constructor, in ct_xex]
PositiveSet.ct_gxg [lemma, in ct_gxg]
PositiveSet.ct_gxg [lemma, in ct_gxg]
PositiveSet.ct_compare [lemma, in ct_compare]
PositiveSet.ct_compare_fun [lemma, in ct_compare_fun]
PositiveSet.ct_compare_bool [lemma, in ct_compare_bool]
PositiveSet.ct_compare_bool [lemma, in ct_compare_bool]
PositiveSet.ct_xll [lemma, in ct_xll]
PositiveSet.ct_xll [lemma, in ct_xll]
PositiveSet.ct_exx [constructor, in ct_exx]
PositiveSet.ct_exx [constructor, in ct_exx]
PositiveSet.ct_lxl [lemma, in ct_lxl]
PositiveSet.ct_lxl [lemma, in ct_lxl]
PositiveSet.ct_xce [lemma, in ct_xce]
PositiveSet.ct_xce [lemma, in ct_xce]
PositiveSet.ct_glx [constructor, in ct_glx]
PositiveSet.ct_glx [constructor, in ct_glx]
PositiveSet.ct_cxe [lemma, in ct_cxe]
PositiveSet.ct_cxe [lemma, in ct_cxe]
PositiveSet.ct_lgx [constructor, in ct_lgx]
PositiveSet.ct_lgx [constructor, in ct_lgx]
PositiveSet.ct_xgg [lemma, in ct_xgg]
PositiveSet.ct_xgg [lemma, in ct_xgg]
PositiveSet.diff [definition, in diff]
PositiveSet.diff [definition, in diff]
PositiveSet.diff_spec [lemma, in diff_spec]
PositiveSet.diff_spec [lemma, in diff_spec]
PositiveSet.diff_2 [lemma, in diff_2]
PositiveSet.diff_1 [lemma, in diff_1]
PositiveSet.diff_3 [lemma, in diff_3]
PositiveSet.E [module, in PositiveSet.E]
PositiveSet.E [module, in PositiveSet.E]
PositiveSet.elements [definition, in elements]
PositiveSet.elements [definition, in elements]
PositiveSet.elements_spec2w [lemma, in elements_spec2w]
PositiveSet.elements_3w [lemma, in elements_3w]
PositiveSet.elements_spec2 [lemma, in elements_spec2]
PositiveSet.elements_3 [lemma, in elements_3]
PositiveSet.elements_spec1 [lemma, in elements_spec1]
PositiveSet.elements_1 [lemma, in elements_1]
PositiveSet.elements_2 [lemma, in elements_2]
PositiveSet.elt [definition, in elt]
PositiveSet.elt [definition, in elt]
PositiveSet.empty [definition, in empty]
PositiveSet.empty [definition, in empty]
PositiveSet.Empty [definition, in Empty]
PositiveSet.Empty [definition, in Empty]
PositiveSet.empty_spec [lemma, in empty_spec]
PositiveSet.empty_1 [lemma, in empty_1]
PositiveSet.eq [definition, in eq]
PositiveSet.eq [definition, in eq]
PositiveSet.equal [definition, in equal]
PositiveSet.equal [definition, in equal]
PositiveSet.Equal [definition, in Equal]
PositiveSet.Equal [definition, in Equal]
PositiveSet.equal_spec [lemma, in equal_spec]
PositiveSet.equal_spec [lemma, in equal_spec]
PositiveSet.equal_2 [lemma, in equal_2]
PositiveSet.equal_1 [lemma, in equal_1]
PositiveSet.equal_subset [lemma, in equal_subset]
PositiveSet.equal_subset [lemma, in equal_subset]
PositiveSet.eq_refl [lemma, in eq_refl]
PositiveSet.eq_sym [lemma, in eq_sym]
PositiveSet.eq_trans [lemma, in eq_trans]
PositiveSet.eq_dec [lemma, in eq_dec]
PositiveSet.eq_dec [lemma, in eq_dec]
PositiveSet.eq_equiv [instance, in eq_equiv]
PositiveSet.Exists [definition, in Exists]
PositiveSet.Exists [definition, in Exists]
PositiveSet.exists_spec [lemma, in exists_spec]
PositiveSet.exists_1 [lemma, in exists_1]
PositiveSet.exists_ [definition, in exists_]
PositiveSet.exists_ [definition, in exists_]
PositiveSet.exists_2 [lemma, in exists_2]
PositiveSet.filter [definition, in filter]
PositiveSet.filter [definition, in filter]
PositiveSet.filter_spec [lemma, in filter_spec]
PositiveSet.filter_1 [lemma, in filter_1]
PositiveSet.filter_3 [lemma, in filter_3]
PositiveSet.filter_2 [lemma, in filter_2]
PositiveSet.Fold [section, in Fold]
PositiveSet.Fold [section, in Fold]
PositiveSet.fold [definition, in fold]
PositiveSet.fold [definition, in fold]
PositiveSet.fold_1 [lemma, in fold_1]
PositiveSet.fold_spec [lemma, in fold_spec]
PositiveSet.Fold.B [variable, in B]
PositiveSet.Fold.B [variable, in B]
PositiveSet.Fold.f [variable, in f]
PositiveSet.Fold.f [variable, in f]
PositiveSet.for_all_1 [lemma, in for_all_1]
PositiveSet.for_all_2 [lemma, in for_all_2]
PositiveSet.For_all [definition, in For_all]
PositiveSet.For_all [definition, in For_all]
PositiveSet.for_all [definition, in for_all]
PositiveSet.for_all [definition, in for_all]
PositiveSet.for_all_spec [lemma, in for_all_spec]
PositiveSet.In [definition, in In]
PositiveSet.In [definition, in In]
PositiveSet.InL [abbreviation, in InL]
PositiveSet.InL [abbreviation, in InL]
PositiveSet.inter [definition, in inter]
PositiveSet.inter [definition, in inter]
PositiveSet.inter_spec [lemma, in inter_spec]
PositiveSet.inter_spec [lemma, in inter_spec]
PositiveSet.inter_3 [lemma, in inter_3]
PositiveSet.inter_2 [lemma, in inter_2]
PositiveSet.inter_1 [lemma, in inter_1]
PositiveSet.In_1 [lemma, in In_1]
PositiveSet.In_compat [instance, in In_compat]
PositiveSet.is_empty_1 [lemma, in is_empty_1]
PositiveSet.is_empty [definition, in is_empty]
PositiveSet.is_empty [definition, in is_empty]
PositiveSet.is_empty_2 [lemma, in is_empty_2]
PositiveSet.is_empty_spec [lemma, in is_empty_spec]
PositiveSet.is_empty_spec [lemma, in is_empty_spec]
PositiveSet.Leaf [constructor, in Leaf]
PositiveSet.Leaf [constructor, in Leaf]
PositiveSet.lex [abbreviation, in lex]
PositiveSet.lex [abbreviation, in lex]
PositiveSet.lex_Eq [lemma, in lex_Eq]
PositiveSet.lex_Eq [lemma, in lex_Eq]
PositiveSet.lex_Opp [lemma, in lex_Opp]
PositiveSet.lex_Opp [lemma, in lex_Opp]
PositiveSet.lt [definition, in lt]
PositiveSet.lt [definition, in lt]
PositiveSet.lt_compat [instance, in lt_compat]
PositiveSet.lt_strorder [instance, in lt_strorder]
PositiveSet.lt_rev_append [lemma, in lt_rev_append]
PositiveSet.lt_rev_append [lemma, in lt_rev_append]
PositiveSet.lt_spec [section, in lt_spec]
PositiveSet.lt_spec [section, in lt_spec]
PositiveSet.lt_not_eq [lemma, in lt_not_eq]
PositiveSet.lt_trans [lemma, in lt_trans]
PositiveSet.max_elt_spec3 [lemma, in max_elt_spec3]
PositiveSet.max_elt_spec2 [lemma, in max_elt_spec2]
PositiveSet.max_elt [definition, in max_elt]
PositiveSet.max_elt [definition, in max_elt]
PositiveSet.max_elt_1 [lemma, in max_elt_1]
PositiveSet.max_elt_3 [lemma, in max_elt_3]
PositiveSet.max_elt_spec1 [lemma, in max_elt_spec1]
PositiveSet.max_elt_2 [lemma, in max_elt_2]
PositiveSet.mem [definition, in mem]
PositiveSet.mem [definition, in mem]
PositiveSet.mem_node [lemma, in mem_node]
PositiveSet.mem_node [lemma, in mem_node]
PositiveSet.mem_Leaf [lemma, in mem_Leaf]
PositiveSet.mem_Leaf [lemma, in mem_Leaf]
PositiveSet.mem_1 [lemma, in mem_1]
PositiveSet.mem_2 [lemma, in mem_2]
PositiveSet.mem_spec [lemma, in mem_spec]
PositiveSet.min_elt_3 [lemma, in min_elt_3]
PositiveSet.min_elt_spec2 [lemma, in min_elt_spec2]
PositiveSet.min_elt_2 [lemma, in min_elt_2]
PositiveSet.min_elt_spec3 [lemma, in min_elt_spec3]
PositiveSet.min_elt_1 [lemma, in min_elt_1]
PositiveSet.min_elt_spec1 [lemma, in min_elt_spec1]
PositiveSet.min_elt [definition, in min_elt]
PositiveSet.min_elt [definition, in min_elt]
PositiveSet.Node [constructor, in Node]
PositiveSet.Node [constructor, in Node]
PositiveSet.node [definition, in node]
PositiveSet.node [definition, in node]
PositiveSet.omap [definition, in omap]
PositiveSet.omap [definition, in omap]
PositiveSet.partition [definition, in partition]
PositiveSet.partition [definition, in partition]
PositiveSet.partition_spec2 [lemma, in partition_spec2]
PositiveSet.partition_spec1 [lemma, in partition_spec1]
PositiveSet.partition_1 [lemma, in partition_1]
PositiveSet.partition_2 [lemma, in partition_2]
PositiveSet.partition_filter [lemma, in partition_filter]
PositiveSet.partition_filter [lemma, in partition_filter]
PositiveSet.Quantifiers [section, in Quantifiers]
PositiveSet.Quantifiers [section, in Quantifiers]
PositiveSet.Quantifiers.f [variable, in f]
PositiveSet.Quantifiers.f [variable, in f]
PositiveSet.remove [definition, in remove]
PositiveSet.remove [definition, in remove]
PositiveSet.remove_spec [lemma, in remove_spec]
PositiveSet.remove_spec [lemma, in remove_spec]
PositiveSet.remove_2 [lemma, in remove_2]
PositiveSet.remove_1 [lemma, in remove_1]
PositiveSet.remove_3 [lemma, in remove_3]
PositiveSet.rev [definition, in rev]
PositiveSet.rev [definition, in rev]
PositiveSet.rev_append [definition, in rev_append]
PositiveSet.rev_append [definition, in rev_append]
PositiveSet.singleton [definition, in singleton]
PositiveSet.singleton [definition, in singleton]
PositiveSet.singleton_spec [lemma, in singleton_spec]
PositiveSet.singleton_1 [lemma, in singleton_1]
PositiveSet.singleton_2 [lemma, in singleton_2]
PositiveSet.Subset [definition, in Subset]
PositiveSet.Subset [definition, in Subset]
PositiveSet.subset [definition, in subset]
PositiveSet.subset [definition, in subset]
PositiveSet.subset_spec [lemma, in subset_spec]
PositiveSet.subset_spec [lemma, in subset_spec]
PositiveSet.subset_2 [lemma, in subset_2]
PositiveSet.subset_1 [lemma, in subset_1]
PositiveSet.subset_Leaf_s [lemma, in subset_Leaf_s]
PositiveSet.subset_Leaf_s [lemma, in subset_Leaf_s]
PositiveSet.t [definition, in t]
PositiveSet.t [definition, in t]
PositiveSet.tree [inductive, in tree]
PositiveSet.tree [inductive, in tree]
PositiveSet.tree_ind [definition, in tree_ind]
PositiveSet.tree_ind [definition, in tree_ind]
PositiveSet.union [definition, in union]
PositiveSet.union [definition, in union]
PositiveSet.union_1 [lemma, in union_1]
PositiveSet.union_2 [lemma, in union_2]
PositiveSet.union_spec [lemma, in union_spec]
PositiveSet.union_spec [lemma, in union_spec]
PositiveSet.union_3 [lemma, in union_3]
PositiveSet.xelements [definition, in xelements]
PositiveSet.xelements [definition, in xelements]
PositiveSet.xelements_spec [lemma, in xelements_spec]
PositiveSet.xelements_spec [lemma, in xelements_spec]
PositiveSet.xexists [definition, in xexists]
PositiveSet.xexists [definition, in xexists]
PositiveSet.xexists_spec [lemma, in xexists_spec]
PositiveSet.xexists_spec [lemma, in xexists_spec]
PositiveSet.xfilter [definition, in xfilter]
PositiveSet.xfilter [definition, in xfilter]
PositiveSet.xfilter_spec [lemma, in xfilter_spec]
PositiveSet.xfilter_spec [lemma, in xfilter_spec]
PositiveSet.xfold [definition, in xfold]
PositiveSet.xfold [definition, in xfold]
PositiveSet.xforall [definition, in xforall]
PositiveSet.xforall [definition, in xforall]
PositiveSet.xforall_spec [lemma, in xforall_spec]
PositiveSet.xforall_spec [lemma, in xforall_spec]
PositiveSet.xpartition [definition, in xpartition]
PositiveSet.xpartition [definition, in xpartition]
_ [=] _ [notation, in ::x_'[=]'_x]
_ [=] _ [notation, in ::x_'[=]'_x]
_ [<=] _ [notation, in ::x_'[<=]'_x]
_ [<=] _ [notation, in ::x_'[<=]'_x]
_ @ _ [notation, in ::x_'@'_x]
_ @ _ [notation, in ::x_'@'_x]
positive_derivative [lemma, in positive_derivative]
Positive_as_OT.eq_refl [definition, in eq_refl]
positive_mask_ind [abbreviation, in positive_mask_ind]
positive_mask_rect [abbreviation, in positive_mask_rect]
positive_rec [abbreviation, in positive_rec]
positive_nat_N [lemma, in positive_nat_N]
Positive_as_OT.t [definition, in t]
positive_N_nat [lemma, in positive_N_nat]
Positive_as_OT.compare [definition, in compare]
positive_to_int31_spec [lemma, in positive_to_int31_spec]
positive_N_Z [lemma, in positive_N_Z]
positive_mask [abbreviation, in positive_mask]
Positive_as_OT [module, in Positive_as_OT]
Positive_as_OT [module, in Positive_as_OT]
Positive_as_OT [module, in Positive_as_OT]
Positive_as_OT.eq_sym [definition, in eq_sym]
positive_to_int31_phi_inv_positive [lemma, in positive_to_int31_phi_inv_positive]
Positive_as_OT.lt_not_eq [lemma, in lt_not_eq]
Positive_as_DT [module, in Positive_as_DT]
Positive_as_DT [module, in Positive_as_DT]
Positive_as_DT [module, in Positive_as_DT]
positive_mask_rec [abbreviation, in positive_mask_rec]
positive_ind [abbreviation, in positive_ind]
Positive_as_OT.lt_trans [definition, in lt_trans]
Positive_as_OT.eq_trans [definition, in eq_trans]
Positive_as_OT.eq_dec [definition, in eq_dec]
positive_nat_Z [lemma, in positive_nat_Z]
positive_to_int31 [definition, in positive_to_int31]
Positive_as_OT.lt [definition, in lt]
positive_rect [abbreviation, in positive_rect]
Positive_as_OT.eq [definition, in eq]
positive_eq_dec [abbreviation, in positive_eq_dec]
positivity_seq [definition, in positivity_seq]
posreal [record, in posreal]
pos_INR_nat_of_P [lemma, in pos_INR_nat_of_P]
POS_MOD.spec_ww_digits [variable, in spec_ww_digits]
POS_MOD.spec_low [variable, in spec_low]
POS_MOD.spec_to_w_Z [variable, in spec_to_w_Z]
POS_MOD.spec_w_0 [variable, in spec_w_0]
POS_MOD.ww_zdigits [variable, in ww_zdigits]
[[ _ ]] [notation, in ::'[['_x_']]']
POS_MOD.spec_ww_sub [variable, in spec_ww_sub]
pos_opp_lt [lemma, in pos_opp_lt]
POS_MOD.w_digits [variable, in w_digits]
POS_MOD.spec_zdigits [variable, in spec_zdigits]
pos_Rl_P1 [lemma, in pos_Rl_P1]
POS_MOD.w_pos_mod [variable, in w_pos_mod]
pos_INR [lemma, in pos_INR]
POS_MOD.w_compare [variable, in w_compare]
pos_half_prf [definition, in pos_half_prf]
POS_MOD.spec_w_WW [variable, in spec_w_WW]
POS_MOD.w_to_Z [variable, in w_to_Z]
pos_half [definition, in pos_half]
POS_MOD.spec_ww_zdigits [variable, in spec_ww_zdigits]
POS_MOD.spec_ww_compare [variable, in spec_ww_compare]
POS_MOD [section, in POS_MOD]
POS_MOD.spec_to_Z [variable, in spec_to_Z]
POS_MOD.spec_pos_mod [variable, in spec_pos_mod]
[| _ |] [notation, in ::'[|'_x_'|]']
POS_MOD.w_WW [variable, in w_WW]
pos_Rl [definition, in pos_Rl]
POS_MOD.ww_compare [variable, in ww_compare]
POS_MOD.w_0 [variable, in w_0]
pos_mod [definition, in pos_mod]
pos_Rl_P2 [lemma, in pos_Rl_P2]
POS_MOD.w [variable, in w]
POS_MOD.low [variable, in low]
POS_MOD.spec_w_0W [variable, in spec_w_0W]
POS_MOD.ww_sub [variable, in ww_sub]
POS_MOD.w_0W [variable, in w_0W]
POS_MOD.w_zdigits [variable, in w_zdigits]
Pos.add [definition, in add]
Pos.add_xO [lemma, in add_xO]
Pos.add_1_r [lemma, in add_1_r]
Pos.add_diag [lemma, in add_diag]
Pos.add_succ_r [lemma, in add_succ_r]
Pos.add_succ_l [lemma, in add_succ_l]
Pos.add_sub_assoc [lemma, in add_sub_assoc]
Pos.add_carry_add [lemma, in add_carry_add]
Pos.add_max_distr_r [lemma, in add_max_distr_r]
Pos.add_cancel_l [lemma, in add_cancel_l]
Pos.add_reg_l [lemma, in add_reg_l]
Pos.add_compare_mono_r [lemma, in add_compare_mono_r]
Pos.add_min_distr_r [lemma, in add_min_distr_r]
Pos.add_carry_spec [lemma, in add_carry_spec]
Pos.add_lt_mono [lemma, in add_lt_mono]
Pos.add_assoc [lemma, in add_assoc]
Pos.add_no_neutral [lemma, in add_no_neutral]
Pos.add_comm [lemma, in add_comm]
Pos.add_le_mono_r [lemma, in add_le_mono_r]
Pos.add_reg_r [lemma, in add_reg_r]
Pos.add_sub [lemma, in add_sub]
Pos.add_carry_reg_r [lemma, in add_carry_reg_r]
Pos.add_carry [definition, in add_carry]
Pos.add_1_l [lemma, in add_1_l]
Pos.add_cancel_r [lemma, in add_cancel_r]
Pos.add_compare_mono_l [lemma, in add_compare_mono_l]
Pos.add_carry_reg_l [lemma, in add_carry_reg_l]
Pos.add_lt_mono_l [lemma, in add_lt_mono_l]
Pos.add_le_mono_l [lemma, in add_le_mono_l]
Pos.add_xO_pred_double [lemma, in add_xO_pred_double]
Pos.add_min_distr_l [lemma, in add_min_distr_l]
Pos.add_xI_pred_double [lemma, in add_xI_pred_double]
Pos.add_le_mono [lemma, in add_le_mono]
Pos.add_lt_mono_r [lemma, in add_lt_mono_r]
Pos.add_max_distr_l [lemma, in add_max_distr_l]
Pos.compare [definition, in compare]
Pos.compare_lt_iff [lemma, in compare_lt_iff]
Pos.compare_cont [definition, in compare_cont]
Pos.compare_sub_mask [lemma, in compare_sub_mask]
Pos.compare_antisym [lemma, in compare_antisym]
Pos.compare_succ_l [lemma, in compare_succ_l]
Pos.compare_xO_xI [lemma, in compare_xO_xI]
Pos.compare_xI_xI [lemma, in compare_xI_xI]
Pos.compare_cont_refl [lemma, in compare_cont_refl]
Pos.compare_succ_r [lemma, in compare_succ_r]
Pos.compare_succ_succ [lemma, in compare_succ_succ]
Pos.compare_cont_Lt_Lt [lemma, in compare_cont_Lt_Lt]
Pos.compare_le_iff [lemma, in compare_le_iff]
Pos.compare_cont_Gt_Gt [lemma, in compare_cont_Gt_Gt]
Pos.compare_cont_Lt_Gt [lemma, in compare_cont_Lt_Gt]
Pos.compare_eq_iff [lemma, in compare_eq_iff]
Pos.compare_cont_spec [lemma, in compare_cont_spec]
Pos.compare_cont_Eq [lemma, in compare_cont_Eq]
Pos.compare_xI_xO [lemma, in compare_xI_xO]
Pos.compare_cont_Gt_Lt [lemma, in compare_cont_Gt_Lt]
Pos.compare_cont_antisym [lemma, in compare_cont_antisym]
Pos.compare_xO_xO [lemma, in compare_xO_xO]
Pos.divide [definition, in divide]
Pos.divide_xO_xO [lemma, in divide_xO_xO]
Pos.divide_add_cancel_l [lemma, in divide_add_cancel_l]
Pos.divide_xO_xI [lemma, in divide_xO_xI]
Pos.divide_mul_l [lemma, in divide_mul_l]
Pos.divide_mul_r [lemma, in divide_mul_r]
Pos.div2 [definition, in div2]
Pos.div2_up [definition, in div2_up]
Pos.double_succ [lemma, in double_succ]
Pos.double_mask [definition, in double_mask]
Pos.double_pred_mask [definition, in double_pred_mask]
Pos.eq [definition, in eq]
Pos.eqb [definition, in eqb]
Pos.eqb_eq [lemma, in eqb_eq]
Pos.eq_dep_eq_positive [lemma, in eq_dep_eq_positive]
Pos.eq_dec [lemma, in eq_dec]
Pos.eq_equiv [definition, in eq_equiv]
Pos.gcd [definition, in gcd]
Pos.gcdn [definition, in gcdn]
Pos.gcdn_greatest [lemma, in gcdn_greatest]
Pos.gcd_greatest [lemma, in gcd_greatest]
Pos.gcd_divide_r [lemma, in gcd_divide_r]
Pos.gcd_divide_l [lemma, in gcd_divide_l]
Pos.ge [definition, in ge]
Pos.ge_le [lemma, in ge_le]
Pos.ge_le_iff [lemma, in ge_le_iff]
Pos.ggcd [definition, in ggcd]
Pos.ggcdn [definition, in ggcdn]
Pos.ggcdn_correct_divisors [lemma, in ggcdn_correct_divisors]
Pos.ggcdn_gcdn [lemma, in ggcdn_gcdn]
Pos.ggcd_greatest [lemma, in ggcd_greatest]
Pos.ggcd_correct_divisors [lemma, in ggcd_correct_divisors]
Pos.ggcd_gcd [lemma, in ggcd_gcd]
Pos.gt [definition, in gt]
Pos.gt_iff_add [lemma, in gt_iff_add]
Pos.gt_lt [lemma, in gt_lt]
Pos.gt_lt_iff [lemma, in gt_lt_iff]
Pos.IsNeg [constructor, in IsNeg]
Pos.IsNul [constructor, in IsNul]
Pos.IsPos [constructor, in IsPos]
Pos.iter [definition, in iter]
Pos.iter_invariant [lemma, in iter_invariant]
Pos.iter_op [definition, in iter_op]
Pos.iter_swap [lemma, in iter_swap]
Pos.iter_succ [lemma, in iter_succ]
Pos.iter_add [lemma, in iter_add]
Pos.iter_op_succ [lemma, in iter_op_succ]
Pos.iter_swap_gen [lemma, in iter_swap_gen]
Pos.land [definition, in land]
Pos.ldiff [definition, in ldiff]
Pos.le [definition, in le]
Pos.leb [definition, in leb]
Pos.leb_le [lemma, in leb_le]
Pos.le_lteq [definition, in le_lteq]
Pos.le_nlt [lemma, in le_nlt]
Pos.le_1_l [lemma, in le_1_l]
Pos.le_trans [lemma, in le_trans]
Pos.le_preorder [instance, in le_preorder]
Pos.le_partorder [instance, in le_partorder]
Pos.le_ge [lemma, in le_ge]
Pos.le_antisym [lemma, in le_antisym]
Pos.le_succ_l [lemma, in le_succ_l]
Pos.le_lt_trans [lemma, in le_lt_trans]
Pos.le_refl [lemma, in le_refl]
Pos.lor [definition, in lor]
Pos.lt [definition, in lt]
Pos.ltb [definition, in ltb]
Pos.ltb_lt [lemma, in ltb_lt]
Pos.lt_le_incl [lemma, in lt_le_incl]
Pos.lt_compat [instance, in lt_compat]
Pos.lt_strorder [instance, in lt_strorder]
Pos.lt_add_diag_r [lemma, in lt_add_diag_r]
Pos.lt_lt_succ [lemma, in lt_lt_succ]
Pos.lt_ind [lemma, in lt_ind]
Pos.lt_iff_add [lemma, in lt_iff_add]
Pos.lt_add_r [lemma, in lt_add_r]
Pos.lt_le_trans [lemma, in lt_le_trans]
Pos.lt_nle [lemma, in lt_nle]
Pos.lt_1_succ [lemma, in lt_1_succ]
Pos.lt_total [lemma, in lt_total]
Pos.lt_succ_r [lemma, in lt_succ_r]
Pos.lt_trans [lemma, in lt_trans]
Pos.lt_succ_diag_r [lemma, in lt_succ_diag_r]
Pos.lt_gt [lemma, in lt_gt]
Pos.lt_not_add_l [lemma, in lt_not_add_l]
Pos.lxor [definition, in lxor]
Pos.mask [inductive, in mask]
Pos.mask2cmp [definition, in mask2cmp]
Pos.max [definition, in max]
Pos.max_r [lemma, in max_r]
Pos.max_1_r [lemma, in max_1_r]
Pos.max_1_l [lemma, in max_1_l]
Pos.max_l [lemma, in max_l]
Pos.min [definition, in min]
Pos.min_1_l [lemma, in min_1_l]
Pos.min_r [lemma, in min_r]
Pos.min_l [lemma, in min_l]
Pos.min_1_r [lemma, in min_1_r]
Pos.mul [definition, in mul]
Pos.mul_min_distr_r [lemma, in mul_min_distr_r]
Pos.mul_xI_mul_xO_discr [lemma, in mul_xI_mul_xO_discr]
Pos.mul_compare_mono_l [lemma, in mul_compare_mono_l]
Pos.mul_1_r [lemma, in mul_1_r]
Pos.mul_add_distr_l [lemma, in mul_add_distr_l]
Pos.mul_le_mono [lemma, in mul_le_mono]
Pos.mul_xO_r [lemma, in mul_xO_r]
Pos.mul_eq_1_r [lemma, in mul_eq_1_r]
Pos.mul_sub_distr_r [lemma, in mul_sub_distr_r]
Pos.mul_compare_mono_r [lemma, in mul_compare_mono_r]
Pos.mul_reg_l [lemma, in mul_reg_l]
Pos.mul_sub_distr_l [lemma, in mul_sub_distr_l]
Pos.mul_xO_discr [lemma, in mul_xO_discr]
Pos.mul_lt_mono [lemma, in mul_lt_mono]
Pos.mul_lt_mono_l [lemma, in mul_lt_mono_l]
Pos.mul_eq_1_l [lemma, in mul_eq_1_l]
Pos.mul_succ_l [lemma, in mul_succ_l]
Pos.mul_1_l [lemma, in mul_1_l]
Pos.mul_succ_r [lemma, in mul_succ_r]
Pos.mul_reg_r [lemma, in mul_reg_r]
Pos.mul_cancel_l [lemma, in mul_cancel_l]
Pos.mul_lt_mono_r [lemma, in mul_lt_mono_r]
Pos.mul_add_distr_r [lemma, in mul_add_distr_r]
Pos.mul_le_mono_r [lemma, in mul_le_mono_r]
Pos.mul_max_distr_r [lemma, in mul_max_distr_r]
Pos.mul_cancel_r [lemma, in mul_cancel_r]
Pos.mul_comm [lemma, in mul_comm]
Pos.mul_max_distr_l [lemma, in mul_max_distr_l]
Pos.mul_le_mono_l [lemma, in mul_le_mono_l]
Pos.mul_eq_1 [abbreviation, in mul_eq_1]
Pos.mul_assoc [lemma, in mul_assoc]
Pos.mul_min_distr_l [lemma, in mul_min_distr_l]
Pos.mul_xI_r [lemma, in mul_xI_r]
Pos.Ndouble [definition, in Ndouble]
Pos.nlt_1_r [lemma, in nlt_1_r]
Pos.Nsucc_double [definition, in Nsucc_double]
Pos.of_nat [definition, in of_nat]
Pos.of_succ_nat [definition, in of_succ_nat]
Pos.of_nat_succ [lemma, in of_nat_succ]
Pos.PeanoOne [constructor, in PeanoOne]
Pos.PeanoSucc [constructor, in PeanoSucc]
Pos.peanoView [definition, in peanoView]
Pos.PeanoView [inductive, in PeanoView]
Pos.PeanoViewUnique [lemma, in PeanoViewUnique]
Pos.PeanoView_iter [definition, in PeanoView_iter]
Pos.peanoView_xI [definition, in peanoView_xI]
Pos.peanoView_xO [definition, in peanoView_xO]
Pos.peano_ind [definition, in peano_ind]
Pos.peano_rec [definition, in peano_rec]
Pos.peano_rect_succ [lemma, in peano_rect_succ]
Pos.peano_rect_base [lemma, in peano_rect_base]
Pos.peano_equiv [lemma, in peano_equiv]
Pos.peano_rect [definition, in peano_rect]
Pos.peano_case [lemma, in peano_case]
Pos.pow [definition, in pow]
Pos.pow_1_r [lemma, in pow_1_r]
Pos.pow_succ_r [lemma, in pow_succ_r]
Pos.pow_gt_1 [lemma, in pow_gt_1]
Pos.pred [definition, in pred]
Pos.pred_N_succ [lemma, in pred_N_succ]
Pos.pred_double [definition, in pred_double]
Pos.pred_double_spec [lemma, in pred_double_spec]
Pos.pred_N [definition, in pred_N]
Pos.pred_sub [lemma, in pred_sub]
Pos.pred_succ [lemma, in pred_succ]
Pos.pred_mask [definition, in pred_mask]
Pos.pred_double_succ [lemma, in pred_double_succ]
Pos.pred_double_xO_discr [lemma, in pred_double_xO_discr]
Pos.pred_of_succ_nat [lemma, in pred_of_succ_nat]
Pos.shiftl [definition, in shiftl]
Pos.shiftl_nat [definition, in shiftl_nat]
Pos.shiftr [definition, in shiftr]
Pos.shiftr_nat [definition, in shiftr_nat]
Pos.size [definition, in size]
Pos.size_gt [lemma, in size_gt]
Pos.size_le [lemma, in size_le]
Pos.size_nat [definition, in size_nat]
Pos.size_nat_monotone [lemma, in size_nat_monotone]
Pos.sqrt [definition, in sqrt]
Pos.SqrtApprox [constructor, in SqrtApprox]
Pos.SqrtExact [constructor, in SqrtExact]
Pos.sqrtrem [definition, in sqrtrem]
Pos.sqrtrem_step_spec [lemma, in sqrtrem_step_spec]
Pos.sqrtrem_step [definition, in sqrtrem_step]
Pos.sqrtrem_spec [lemma, in sqrtrem_spec]
Pos.SqrtSpec [inductive, in SqrtSpec]
Pos.sqrt_spec [lemma, in sqrt_spec]
Pos.square [definition, in square]
Pos.square_spec [lemma, in square_spec]
Pos.square_xI [lemma, in square_xI]
Pos.square_xO [lemma, in square_xO]
Pos.sub [definition, in sub]
Pos.SubIsNeg [constructor, in SubIsNeg]
Pos.SubIsNul [constructor, in SubIsNul]
Pos.SubIsPos [constructor, in SubIsPos]
Pos.SubMaskSpec [inductive, in SubMaskSpec]
Pos.sub_mask_carry_spec [lemma, in sub_mask_carry_spec]
Pos.sub_mask_neg_iff' [lemma, in sub_mask_neg_iff']
Pos.sub_compare_mono_r [lemma, in sub_compare_mono_r]
Pos.sub_lt_mono_l [lemma, in sub_lt_mono_l]
Pos.sub_decr [lemma, in sub_decr]
Pos.sub_le [lemma, in sub_le]
Pos.sub_sub_distr [lemma, in sub_sub_distr]
Pos.sub_mask_spec [lemma, in sub_mask_spec]
Pos.sub_xO_xI [lemma, in sub_xO_xI]
Pos.sub_xO_xO [lemma, in sub_xO_xO]
Pos.sub_1_r [lemma, in sub_1_r]
Pos.sub_add [lemma, in sub_add]
Pos.sub_xI_xO [lemma, in sub_xI_xO]
Pos.sub_mask_pos [lemma, in sub_mask_pos]
Pos.sub_lt_mono_r [lemma, in sub_lt_mono_r]
Pos.sub_mask_pos' [lemma, in sub_mask_pos']
Pos.sub_diag [lemma, in sub_diag]
Pos.sub_mask_neg [lemma, in sub_mask_neg]
Pos.sub_mask_add [lemma, in sub_mask_add]
Pos.sub_xI_xI [lemma, in sub_xI_xI]
Pos.sub_mask_nul_iff [lemma, in sub_mask_nul_iff]
Pos.sub_mask_add_diag_r [lemma, in sub_mask_add_diag_r]
Pos.sub_lt [lemma, in sub_lt]
Pos.sub_mask_succ_r [lemma, in sub_mask_succ_r]
Pos.sub_mask_carry [definition, in sub_mask_carry]
Pos.sub_mask_add_diag_l [lemma, in sub_mask_add_diag_l]
Pos.sub_mask_pos_iff [lemma, in sub_mask_pos_iff]
Pos.sub_mask_neg_iff [lemma, in sub_mask_neg_iff]
Pos.sub_mask [definition, in sub_mask]
Pos.sub_succ_r [lemma, in sub_succ_r]
Pos.sub_add_distr [lemma, in sub_add_distr]
Pos.sub_mask_diag [lemma, in sub_mask_diag]
Pos.sub_compare_mono_l [lemma, in sub_compare_mono_l]
Pos.succ [definition, in succ]
Pos.succ_inj [lemma, in succ_inj]
Pos.succ_pred_or [lemma, in succ_pred_or]
Pos.succ_pred_double [lemma, in succ_pred_double]
Pos.succ_not_1 [lemma, in succ_not_1]
Pos.succ_of_nat [lemma, in succ_of_nat]
Pos.succ_double_mask [definition, in succ_double_mask]
Pos.succ_lt_mono [lemma, in succ_lt_mono]
Pos.succ_le_mono [lemma, in succ_le_mono]
Pos.succ_discr [lemma, in succ_discr]
Pos.succ_min_distr [lemma, in succ_min_distr]
Pos.succ_pred [lemma, in succ_pred]
Pos.succ_max_distr [lemma, in succ_max_distr]
Pos.switch_Eq [definition, in switch_Eq]
Pos.t [definition, in t]
Pos.testbit [definition, in testbit]
Pos.testbit_nat [definition, in testbit_nat]
Pos.to_nat [definition, in to_nat]
Pos.xI_succ_xO [lemma, in xI_succ_xO]
( _ | _ ) (positive_scope) [notation, in :positive_scope:'('_x_'|'_x_')']
_ ?= _ (positive_scope) [notation, in :positive_scope:x_'?='_x]
_ =? _ (positive_scope) [notation, in :positive_scope:x_'=?'_x]
_ >= _ (positive_scope) [notation, in :positive_scope:x_'>='_x]
_ > _ (positive_scope) [notation, in :positive_scope:x_'>'_x]
_ - _ (positive_scope) [notation, in :positive_scope:x_'-'_x]
_ < _ <= _ (positive_scope) [notation, in :positive_scope:x_'<'_x_'<='_x]
_ * _ (positive_scope) [notation, in :positive_scope:x_'*'_x]
_ < _ < _ (positive_scope) [notation, in :positive_scope:x_'<'_x_'<'_x]
_ <= _ <= _ (positive_scope) [notation, in :positive_scope:x_'<='_x_'<='_x]
_ <=? _ (positive_scope) [notation, in :positive_scope:x_'<=?'_x]
_ + _ (positive_scope) [notation, in :positive_scope:x_'+'_x]
_ <= _ < _ (positive_scope) [notation, in :positive_scope:x_'<='_x_'<'_x]
_ [notation, in :positive_scope:x_']
_ ^ _ (positive_scope) [notation, in :positive_scope:x_'^'_x]
_ <= _ (positive_scope) [notation, in :positive_scope:x_'<='_x]
_ < _ (positive_scope) [notation, in :positive_scope:x_'<'_x]
Pos2Nat [module, in Pos2Nat]
Pos2Nat.id [lemma, in id]
Pos2Nat.inj [lemma, in inj]
Pos2Nat.inj_max [lemma, in inj_max]
Pos2Nat.inj_lt [lemma, in inj_lt]
Pos2Nat.inj_mul [lemma, in inj_mul]
Pos2Nat.inj_xI [lemma, in inj_xI]
Pos2Nat.inj_pred_max [lemma, in inj_pred_max]
Pos2Nat.inj_iff [lemma, in inj_iff]
Pos2Nat.inj_iter [lemma, in inj_iter]
Pos2Nat.inj_add [lemma, in inj_add]
Pos2Nat.inj_ge [lemma, in inj_ge]
Pos2Nat.inj_compare [lemma, in inj_compare]
Pos2Nat.inj_sub [lemma, in inj_sub]
Pos2Nat.inj_1 [lemma, in inj_1]
Pos2Nat.inj_min [lemma, in inj_min]
Pos2Nat.inj_xO [lemma, in inj_xO]
Pos2Nat.inj_le [lemma, in inj_le]
Pos2Nat.inj_pred [lemma, in inj_pred]
Pos2Nat.inj_succ [lemma, in inj_succ]
Pos2Nat.inj_sub_max [lemma, in inj_sub_max]
Pos2Nat.inj_gt [lemma, in inj_gt]
Pos2Nat.is_succ [lemma, in is_succ]
Pos2Nat.is_pos [lemma, in is_pos]
Pos2SuccNat [module, in Pos2SuccNat]
Pos2SuccNat.id_succ [lemma, in id_succ]
Pos2SuccNat.pred_id [lemma, in pred_id]
Pos2Z [module, in Pos2Z]
Pos2Z.add_neg_pos [lemma, in add_neg_pos]
Pos2Z.add_pos_neg [lemma, in add_pos_neg]
Pos2Z.add_neg_neg [lemma, in add_neg_neg]
Pos2Z.divide_pos_neg_r [lemma, in divide_pos_neg_r]
Pos2Z.divide_pos_neg_l [lemma, in divide_pos_neg_l]
Pos2Z.id [lemma, in id]
Pos2Z.inj [lemma, in inj]
Pos2Z.inj_max [lemma, in inj_max]
Pos2Z.inj_sqrt [lemma, in inj_sqrt]
Pos2Z.inj_mul [lemma, in inj_mul]
Pos2Z.inj_xI [lemma, in inj_xI]
Pos2Z.inj_iff [lemma, in inj_iff]
Pos2Z.inj_leb [lemma, in inj_leb]
Pos2Z.inj_divide [definition, in inj_divide]
Pos2Z.inj_add [lemma, in inj_add]
Pos2Z.inj_gcd [lemma, in inj_gcd]
Pos2Z.inj_compare [lemma, in inj_compare]
Pos2Z.inj_sub [lemma, in inj_sub]
Pos2Z.inj_1 [lemma, in inj_1]
Pos2Z.inj_testbit [lemma, in inj_testbit]
Pos2Z.inj_min [lemma, in inj_min]
Pos2Z.inj_xO [lemma, in inj_xO]
Pos2Z.inj_square [lemma, in inj_square]
Pos2Z.inj_ltb [lemma, in inj_ltb]
Pos2Z.inj_neg [lemma, in inj_neg]
Pos2Z.inj_pred [lemma, in inj_pred]
Pos2Z.inj_succ [lemma, in inj_succ]
Pos2Z.inj_pow [lemma, in inj_pow]
Pos2Z.inj_neg_iff [lemma, in inj_neg_iff]
Pos2Z.inj_sub_max [lemma, in inj_sub_max]
Pos2Z.inj_eqb [lemma, in inj_eqb]
Pos2Z.inj_pow_pos [lemma, in inj_pow_pos]
Pos2Z.is_nonneg [lemma, in is_nonneg]
Pos2Z.is_pos [lemma, in is_pos]
Pos2Z.neg_is_neg [lemma, in neg_is_neg]
Pos2Z.neg_is_nonpos [lemma, in neg_is_nonpos]
Pos2Z.neg_xI [lemma, in neg_xI]
Pos2Z.neg_xO [lemma, in neg_xO]
Pos2Z.opp_neg [lemma, in opp_neg]
Pos2Z.opp_pos [lemma, in opp_pos]
Pos2Z.testbit_neg [lemma, in testbit_neg]
Pow [module, in Pow]
Pow [definition, in Pow]
pow [definition, in pow]
pow [definition, in pow]
pow [definition, in pow]
Power [abbreviation, in Power]
powerRZ [definition, in powerRZ]
powerRZ_le [lemma, in powerRZ_le]
powerRZ_add [lemma, in powerRZ_add]
powerRZ_R1 [lemma, in powerRZ_R1]
powerRZ_lt [lemma, in powerRZ_lt]
powerRZ_NOR [lemma, in powerRZ_NOR]
powerRZ_pos_sub [lemma, in powerRZ_pos_sub]
powerRZ_1 [lemma, in powerRZ_1]
powerRZ_O [lemma, in powerRZ_O]
Powerset [library]
Powerset_Classical_facts [library]
Powerset_facts [library]
Powers_of_2 [section, in Powers_of_2]
Power_set_Inhabited [lemma, in Power_set_Inhabited]
Power_set_PO [definition, in Power_set_PO]
Power_monotonic [lemma, in Power_monotonic]
Power_set [inductive, in Power_set]
power_div_with_rest [section, in power_div_with_rest]
PowNotation [module, in PowNotation]
_ ^ _ [notation, in ::x_'^'_x]
pow_1_even [lemma, in pow_1_even]
pow_lt [lemma, in pow_lt]
pow_fct [definition, in pow_fct]
Pow_x_infinity [lemma, in Pow_x_infinity]
pow_2_n_infty [lemma, in pow_2_n_infty]
pow_O [lemma, in pow_O]
pow_1_odd [lemma, in pow_1_odd]
pow_sqr [lemma, in pow_sqr]
pow_nonzero [lemma, in pow_nonzero]
pow_lt_1_compat [lemma, in pow_lt_1_compat]
pow_incr [lemma, in pow_incr]
pow_lt_1_zero [lemma, in pow_lt_1_zero]
pow_0_r [lemma, in pow_0_r]
pow_le [lemma, in pow_le]
pow_1_abs [lemma, in pow_1_abs]
pow_R1 [lemma, in pow_R1]
pow_2_n_neq_R0 [lemma, in pow_2_n_neq_R0]
pow_succ_r [lemma, in pow_succ_r]
pow_ne_zero [lemma, in pow_ne_zero]
pow_2_n_growing [lemma, in pow_2_n_growing]
pow_add [lemma, in pow_add]
pow_1 [lemma, in pow_1]
pow_R1_Rle [lemma, in pow_R1_Rle]
pow_i [lemma, in pow_i]
pow_2_n [definition, in pow_2_n]
pow_Rabs [lemma, in pow_Rabs]
pow_IZR [lemma, in pow_IZR]
pow_maj_Rabs [lemma, in pow_maj_Rabs]
pow_RN_plus [lemma, in pow_RN_plus]
pow_mult [lemma, in pow_mult]
pow_Rsqr [lemma, in pow_Rsqr]
Pow' [module, in Pow']
Pow.pow [axiom, in pow]
pow1 [lemma, in pow1]
pow2_abs [lemma, in pow2_abs]
pow2_ge_0 [lemma, in pow2_ge_0]
PO_of_chain [projection, in PO_of_chain]
PO_of_cpo [projection, in PO_of_cpo]
PO_cond1 [projection, in PO_cond1]
PO_cond2 [projection, in PO_cond2]
Pplength [definition, in Pplength]
Pplus [abbreviation, in Pplus]
Pplus_no_neutral [abbreviation, in Pplus_no_neutral]
Pplus_lt_mono [abbreviation, in Pplus_lt_mono]
Pplus_le_mono [abbreviation, in Pplus_le_mono]
Pplus_one_succ_l [lemma, in Pplus_one_succ_l]
Pplus_xI_double_minus_one [abbreviation, in Pplus_xI_double_minus_one]
Pplus_carry_reg_r [abbreviation, in Pplus_carry_reg_r]
Pplus_comm [abbreviation, in Pplus_comm]
Pplus_xO [abbreviation, in Pplus_xO]
Pplus_succ_permute_r [abbreviation, in Pplus_succ_permute_r]
Pplus_compare_mono_l [abbreviation, in Pplus_compare_mono_l]
Pplus_minus [lemma, in Pplus_minus]
Pplus_minus_assoc [abbreviation, in Pplus_minus_assoc]
Pplus_lt_mono_r [abbreviation, in Pplus_lt_mono_r]
Pplus_compare_mono_r [abbreviation, in Pplus_compare_mono_r]
Pplus_reg_l [abbreviation, in Pplus_reg_l]
Pplus_carry_spec [abbreviation, in Pplus_carry_spec]
Pplus_one_succ_r [lemma, in Pplus_one_succ_r]
Pplus_le_mono_r [abbreviation, in Pplus_le_mono_r]
Pplus_minus_eq [abbreviation, in Pplus_minus_eq]
Pplus_xO_double_minus_one [abbreviation, in Pplus_xO_double_minus_one]
Pplus_diag [abbreviation, in Pplus_diag]
Pplus_lt_mono_l [abbreviation, in Pplus_lt_mono_l]
Pplus_assoc [abbreviation, in Pplus_assoc]
Pplus_carry [abbreviation, in Pplus_carry]
Pplus_reg_r [abbreviation, in Pplus_reg_r]
Pplus_carry_reg_l [abbreviation, in Pplus_carry_reg_l]
Pplus_plus [abbreviation, in Pplus_plus]
Pplus_carry_plus [abbreviation, in Pplus_carry_plus]
Pplus_le_mono_l [abbreviation, in Pplus_le_mono_l]
Pplus_succ_permute_l [abbreviation, in Pplus_succ_permute_l]
Ppow [abbreviation, in Ppow]
Ppow_succ_r [abbreviation, in Ppow_succ_r]
Ppow_gt_1 [abbreviation, in Ppow_gt_1]
Ppow_1_r [abbreviation, in Ppow_1_r]
Ppred [abbreviation, in Ppred]
Ppred_N_spec [abbreviation, in Ppred_N_spec]
Ppred_mask [abbreviation, in Ppred_mask]
Ppred_N [abbreviation, in Ppred_N]
Ppred_succ [abbreviation, in Ppred_succ]
Ppred_Nsucc [abbreviation, in Ppred_Nsucc]
Ppred_minus [lemma, in Ppred_minus]
pre [projection, in pre]
Prec [abbreviation, in Prec]
Prect [abbreviation, in Prect]
Prect_base [abbreviation, in Prect_base]
Prect_succ [abbreviation, in Prect_succ]
pred [definition, in pred]
pred [definition, in pred]
PredExt_RelChoice_imp_EM.rel_choice [variable, in rel_choice]
PredExt_RelChoice_imp_EM [section, in PredExt_RelChoice_imp_EM]
PredExt_RelChoice_imp_EM.pred_extensionality [variable, in pred_extensionality]
predicate [abbreviation, in predicate]
PredicateExtensionality [definition, in PredicateExtensionality]
predicate_implication_preorder [instance, in predicate_implication_preorder]
predicate_intersection [definition, in predicate_intersection]
predicate_union [definition, in predicate_union]
predicate_equivalence_equivalence [instance, in predicate_equivalence_equivalence]
predicate_all [definition, in predicate_all]
predicate_equivalence_pointwise [lemma, in predicate_equivalence_pointwise]
predicate_equivalence [definition, in predicate_equivalence]
predicate_implication_pointwise [lemma, in predicate_implication_pointwise]
predicate_implication [definition, in predicate_implication]
predicate_exists [definition, in predicate_exists]
pred_c [definition, in pred_c]
pred_o_P_of_succ_nat_o_nat_of_P_eq_id [abbreviation, in pred_o_P_of_succ_nat_o_nat_of_P_eq_id]
pred_ext_and_rel_choice_imp_EM [lemma, in pred_ext_and_rel_choice_imp_EM]
pred_of_minus [lemma, in pred_of_minus]
pred_Sn [lemma, in pred_Sn]
prefix [definition, in prefix]
prefix_correct [lemma, in prefix_correct]
Prelude [library]
PreOrder [record, in PreOrder]
Preorder [inductive, in Preorder]
preorder [record, in preorder]
PreOrder_Reflexive [projection, in PreOrder_Reflexive]
PreOrder_Transitive [projection, in PreOrder_Transitive]
PreOrder_inverse [lemma, in PreOrder_inverse]
preord_refl [projection, in preord_refl]
preord_trans [projection, in preord_trans]
pre_cos_bound [lemma, in pre_cos_bound]
pre_sin_bound [lemma, in pre_sin_bound]
pre_atan [definition, in pre_atan]
prime [inductive, in prime]
prime_dec [definition, in prime_dec]
prime_div_prime [lemma, in prime_div_prime]
prime_alt [lemma, in prime_alt]
prime_dec_aux [definition, in prime_dec_aux]
prime_2 [lemma, in prime_2]
prime_divisors [lemma, in prime_divisors]
prime_rel_prime [lemma, in prime_rel_prime]
prime_3 [lemma, in prime_3]
prime_mult [lemma, in prime_mult]
prime_intro [constructor, in prime_intro]
prime_power_prime [lemma, in prime_power_prime]
prime_ge_2 [lemma, in prime_ge_2]
prime' [definition, in prime']
primitive [definition, in primitive]
prod [inductive, in prod]
prodT [abbreviation, in prodT]
prodT_uncurry [abbreviation, in prodT_uncurry]
prodT_ind [abbreviation, in prodT_ind]
prodT_rec [abbreviation, in prodT_rec]
prodT_curry [abbreviation, in prodT_curry]
prodT_rect [abbreviation, in prodT_rect]
prod_curry [definition, in prod_curry]
prod_SO_pos [lemma, in prod_SO_pos]
prod_eqdec [instance, in prod_eqdec]
prod_eqdec [instance, in prod_eqdec]
prod_f_R0 [definition, in prod_f_R0]
prod_neq_R0 [abbreviation, in prod_neq_R0]
prod_curry_uncurry [lemma, in prod_curry_uncurry]
prod_SO_Rle [lemma, in prod_SO_Rle]
prod_uncurry [definition, in prod_uncurry]
prod_SO_split [lemma, in prod_SO_split]
prod_uncurry_curry [lemma, in prod_uncurry_curry]
prod_length [lemma, in prod_length]
prod_f_SO [abbreviation, in prod_f_SO]
Program [library]
Projections [section, in Projections]
projections [section, in projections]
Projections.A [variable, in A]
projections.A [variable, in A]
projections.B [variable, in B]
Projections.P [variable, in P]
projS1 [abbreviation, in projS1]
projS2 [abbreviation, in projS2]
projT1 [definition, in projT1]
projT1_injective [lemma, in projT1_injective]
projT2 [definition, in projT2]
proj1 [lemma, in proj1]
proj1_inf [definition, in proj1_inf]
proj1_sig [definition, in proj1_sig]
proj2 [lemma, in proj2]
proj2_sig [definition, in proj2_sig]
prolongement_C0 [lemma, in prolongement_C0]
ProofIrrelevance [module, in ProofIrrelevance]
ProofIrrelevance [definition, in ProofIrrelevance]
ProofIrrelevance [library]
ProofIrrelevanceFacts [library]
ProofIrrelevanceTheory [module, in ProofIrrelevanceTheory]
ProofIrrelevanceTheory [module, in ProofIrrelevanceTheory]
ProofIrrelevanceTheory.EqdepTheory [module, in ProofIrrelevanceTheory.EqdepTheory]
ProofIrrelevanceTheory.Eq_rect_eq [module, in ProofIrrelevanceTheory.Eq_rect_eq]
ProofIrrelevanceTheory.Eq_rect_eq.eq_rect_eq [lemma, in eq_rect_eq]
ProofIrrelevanceTheory.eq_indd [definition, in eq_indd]
ProofIrrelevanceTheory.subsetT_eq_compat [lemma, in subsetT_eq_compat]
ProofIrrelevanceTheory.subset_eq_compat [lemma, in subset_eq_compat]
ProofIrrelevance.proof_irrelevance [axiom, in proof_irrelevance]
ProofIrrel_RelChoice_imp_EqEM.rel_choice [variable, in rel_choice]
ProofIrrel_RelChoice_imp_EqEM.a1 [variable, in a1]
ProofIrrel_RelChoice_imp_EqEM.a2 [variable, in a2]
ProofIrrel_RelChoice_imp_EqEM [section, in ProofIrrel_RelChoice_imp_EqEM]
ProofIrrel_RelChoice_imp_EqEM.A [variable, in A]
ProofIrrel_RelChoice_imp_EqEM.proof_irrelevance [variable, in proof_irrelevance]
Proof_irrelevance_gen.bool_elim_redr [variable, in bool_elim_redr]
proof_irrelevance_cc [lemma, in proof_irrelevance_cc]
proof_irrel_rel_choice_imp_eq_dec [lemma, in proof_irrel_rel_choice_imp_eq_dec]
proof_irrel_rel_choice_imp_eq_dec' [lemma, in proof_irrel_rel_choice_imp_eq_dec']
Proof_irrelevance_gen.bool_dep_induction [variable, in bool_dep_induction]
Proof_irrelevance_gen.bool_elim [variable, in bool_elim]
Proof_irrelevance_gen.true [variable, in true]
Proof_irrelevance_EM_CC.B [variable, in B]
Proof_irrelevance_gen.bool_elim_redl [variable, in bool_elim_redl]
Proof_irrelevance_EM_CC.or_elim [variable, in or_elim]
Proof_irrelevance_gen.bool [variable, in bool]
Proof_irrelevance_CIC [section, in Proof_irrelevance_CIC]
proof_irrelevance_cci [lemma, in proof_irrelevance_cci]
Proof_irrelevance_EM_CC.or [variable, in or]
Proof_irrelevance_Prop_Ext_CC [section, in Proof_irrelevance_Prop_Ext_CC]
Proof_irrelevance_EM_CC [section, in Proof_irrelevance_EM_CC]
Proof_irrelevance_CCI.em [variable, in em]
Proof_irrelevance_EM_CC.em [variable, in em]
Proof_irrelevance_CCI [section, in Proof_irrelevance_CCI]
Proof_irrelevance_EM_CC.b2 [variable, in b2]
Proof_irrelevance_EM_CC.or_elim_redr [variable, in or_elim_redr]
Proof_irrelevance_EM_CC.or_intror [variable, in or_intror]
Proof_irrelevance_gen [section, in Proof_irrelevance_gen]
Proof_irrelevance_EM_CC.or_introl [variable, in or_introl]
Proof_irrelevance_EM_CC.or_dep_elim [variable, in or_dep_elim]
Proof_irrelevance_EM_CC.or_elim_redl [variable, in or_elim_redl]
Proof_irrelevance_gen.false [variable, in false]
proof_irrelevance [axiom, in proof_irrelevance]
proof_irrelevance [lemma, in proof_irrelevance]
proof_irrelevance [definition, in proof_irrelevance]
proof_irrel [lemma, in proof_irrel]
Proof_irrelevance_EM_CC.b1 [variable, in b1]
Proper [record, in Proper]
Proper [inductive, in Proper]
ProperNotations [module, in ProperNotations]
_ ==> _ (signature_scope) [notation, in :signature_scope:x_'==>'_x]
_ --> _ (signature_scope) [notation, in :signature_scope:x_'-->'_x]
_ ++> _ (signature_scope) [notation, in :signature_scope:x_'++>'_x]
ProperProxy [record, in ProperProxy]
ProperProxy [inductive, in ProperProxy]
Properties [section, in Properties]
Properties [module, in Properties]
Properties [module, in Properties]
Properties [module, in Properties]
Properties.A [variable, in A]
Properties.Clos_Refl_Sym_Trans [section, in Clos_Refl_Sym_Trans]
Properties.Clos_Refl_Trans [section, in Clos_Refl_Trans]
_ * [notation, in ::x_'*']
Properties.Equivalences [section, in Equivalences]
Properties.R [variable, in R]
proper_sym_flip_2 [lemma, in proper_sym_flip_2]
proper_inverse_proper [definition, in proper_inverse_proper]
proper_sym_flip [lemma, in proper_sym_flip]
proper_subrelation_proper [instance, in proper_subrelation_proper]
proper_sym_impl_iff [lemma, in proper_sym_impl_iff]
proper_proxy [projection, in proper_proxy]
proper_proxy [constructor, in proper_proxy]
proper_prf [projection, in proper_prf]
proper_prf [constructor, in proper_prf]
proper_normalizes_proper [lemma, in proper_normalizes_proper]
proper_proper [instance, in proper_proper]
proper_sym_impl_iff_2 [lemma, in proper_sym_impl_iff_2]
proper_proper_proxy [lemma, in proper_proper_proxy]
proper_eq [lemma, in proper_eq]
Props [module, in Props]
Props.BSLeaf [constructor, in BSLeaf]
Props.BSNode [constructor, in BSNode]
Props.bst [inductive, in bst]
Props.bst_ind [definition, in bst_ind]
Props.bst_Ok [instance, in bst_Ok]
Props.Empty [definition, in Empty]
Props.empty_spec [lemma, in empty_spec]
Props.empty_ok [instance, in empty_ok]
Props.Equal [definition, in Equal]
Props.Exists [definition, in Exists]
Props.For_all [definition, in For_all]
Props.gtb_tree_iff [lemma, in gtb_tree_iff]
Props.gtb_tree [definition, in gtb_tree]
Props.gt_tree [definition, in gt_tree]
Props.gt_tree_not_in [lemma, in gt_tree_not_in]
Props.gt_leaf [lemma, in gt_leaf]
Props.gt_tree_trans [lemma, in gt_tree_trans]
Props.gt_tree_compat [instance, in gt_tree_compat]
Props.gt_tree_node [lemma, in gt_tree_node]
Props.In [definition, in In]
Props.InLeft [constructor, in InLeft]
Props.InRight [constructor, in InRight]
Props.InT [inductive, in InT]
Props.In_leaf_iff [lemma, in In_leaf_iff]
Props.In_1 [lemma, in In_1]
Props.In_compat [instance, in In_compat]
Props.In_node_iff [lemma, in In_node_iff]
Props.IsOk [definition, in IsOk]
Props.isok [definition, in isok]
Props.isok_Ok [instance, in isok_Ok]
Props.isok_iff [lemma, in isok_iff]
Props.IsRoot [constructor, in IsRoot]
Props.is_empty_spec [lemma, in is_empty_spec]
Props.ltb_tree [definition, in ltb_tree]
Props.ltb_tree_iff [lemma, in ltb_tree_iff]
Props.lt_tree_not_in [lemma, in lt_tree_not_in]
Props.lt_leaf [lemma, in lt_leaf]
Props.lt_tree_compat [instance, in lt_tree_compat]
Props.lt_tree [definition, in lt_tree]
Props.lt_tree_node [lemma, in lt_tree_node]
Props.lt_tree_trans [lemma, in lt_tree_trans]
Props.mem_spec [lemma, in mem_spec]
Props.MX [module, in Props.MX]
Props.Ok [record, in Ok]
Props.Ok [inductive, in Ok]
Props.ok [projection, in ok]
Props.ok [constructor, in ok]
Props.Subset [definition, in Subset]
Props.tree_ind [definition, in tree_ind]
prop_degen_ext [lemma, in prop_degen_ext]
prop_eps [lemma, in prop_eps]
prop_degeneracy [definition, in prop_degeneracy]
prop_degen_em [lemma, in prop_degen_em]
prop_ext_retract_A_A_imp_A [lemma, in prop_ext_retract_A_A_imp_A]
prop_extensionality [definition, in prop_extensionality]
prop_ext_A_eq_A_imp_A [lemma, in prop_ext_A_eq_A_imp_A]
prop_ext [lemma, in prop_ext]
prop_ext_em_degen [lemma, in prop_ext_em_degen]
provable_prop_extensionality [definition, in provable_prop_extensionality]
provable_prop_ext [lemma, in provable_prop_ext]
pr_nu [lemma, in pr_nu]
pr_nu_var2_interv [lemma, in pr_nu_var2_interv]
pr_nu_var [lemma, in pr_nu_var]
pr_nu_var2 [lemma, in pr_nu_var2]
Pser [definition, in Pser]
PSeries_reg [library]
Pshiftl_nat_0 [lemma, in Pshiftl_nat_0]
Pshiftl_nat_S [lemma, in Pshiftl_nat_S]
Pshiftl_nat_plus [lemma, in Pshiftl_nat_plus]
Pshiftl_nat_N [lemma, in Pshiftl_nat_N]
Pshiftl_nat_Zpower [lemma, in Pshiftl_nat_Zpower]
Psize [abbreviation, in Psize]
Psize_log_inf [lemma, in Psize_log_inf]
Psize_pos [abbreviation, in Psize_pos]
Psize_pos_le [abbreviation, in Psize_pos_le]
Psize_pos_gt [abbreviation, in Psize_pos_gt]
Psize_monotone [abbreviation, in Psize_monotone]
Psquare [abbreviation, in Psquare]
Psquare_correct [abbreviation, in Psquare_correct]
Psquare_xI [abbreviation, in Psquare_xI]
Psquare_xO [abbreviation, in Psquare_xO]
Psucc [abbreviation, in Psucc]
Psucc_not_one [abbreviation, in Psucc_not_one]
Psucc_discr [abbreviation, in Psucc_discr]
Psucc_pred [abbreviation, in Psucc_pred]
Psucc_inj [abbreviation, in Psucc_inj]
Psucc_o_double_minus_one_eq_xO [abbreviation, in Psucc_o_double_minus_one_eq_xO]
Psucc_S [abbreviation, in Psucc_S]
ps_atan [definition, in ps_atan]
ps_atan_exists_1_opp [lemma, in ps_atan_exists_1_opp]
ps_atan_opp [lemma, in ps_atan_opp]
ps_atan_continuity_pt_1 [lemma, in ps_atan_continuity_pt_1]
ps_atan0_0 [lemma, in ps_atan0_0]
ps_atanSeq_continuity_pt_1 [lemma, in ps_atanSeq_continuity_pt_1]
ps_atan_exists_01 [definition, in ps_atan_exists_01]
ps_atan_exists_1 [definition, in ps_atan_exists_1]
Ptail [definition, in Ptail]
Ptail_pos [lemma, in Ptail_pos]
Ptail_bounded [lemma, in Ptail_bounded]
Ptestbit_Pbit [lemma, in Ptestbit_Pbit]
Pxor [abbreviation, in Pxor]
Pxor_semantics [lemma, in Pxor_semantics]
P_of_succ_nat_of_P [abbreviation, in P_of_succ_nat_of_P]
P_of_succ_nat_o_nat_of_P_eq_succ [abbreviation, in P_of_succ_nat_o_nat_of_P_eq_succ]
P_Rmin [lemma, in P_Rmin]
P_implies_acc [lemma, in P_implies_acc]
P_of_succ_nat [abbreviation, in P_of_succ_nat]
P_nth [inductive, in P_nth]
P_eventually_implies_acc_ex [lemma, in P_eventually_implies_acc_ex]
P_eventually_implies_acc [lemma, in P_eventually_implies_acc]
p_lt_double_digits [lemma, in p_lt_double_digits]
P' [definition, in P']
P'_decidable [lemma, in P'_decidable]
p2b [definition, in p2b]
P2Bv [definition, in P2Bv]
p2i [definition, in p2i]
p2ibis [definition, in p2ibis]
p2ibis_spec [lemma, in p2ibis_spec]
p2ibis_bounded [lemma, in p2ibis_bounded]
p2i_p2ibis [lemma, in p2i_p2ibis]
p2p1 [lemma, in p2p1]
p2p2 [lemma, in p2p2]



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 (18816 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 (644 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 (708 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 (1456 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 (407 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 (8932 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 (422 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 (699 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 (209 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 (203 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 (550 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 (338 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 (1235 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 (2946 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 (67 entries)