Coq.ZArith.Zwf

Global Index

(7984 entries)

Axiom Index

B

H

K

Q

V

W

X

Y

(401 entries)

Lemma Index

Y

(5228 entries)

Constructor Index

K

Q

W

Y

_

(292 entries)

Inductive Index

K

Y

_

(184 entries)

Definition Index

J

_

(1519 entries)

Module Index

A

B

C

G

H

J

L

Q

T

V

W

X

Y

_

(85 entries)

Library Index

K

V

X

Y

_

(275 entries)

P

pair [constructor, in Coq.Init.Datatypes]
PairOrderedType [module, in Coq.FSets.OrderedTypeEx]
pair_sp [lemma, in Coq.IntMap.Mapiter]
paradox [lemma, in Coq.Logic.Hurkens]
Params [library]
Partial_Order [library]
partition [axiom, in Coq.FSets.FSetWeakInterface]
partition [definition, in Coq.Lists.List]
partition [axiom, in Coq.FSets.FSetInterface]
partition [axiom, in Coq.FSets.FSetInterface]
partition_1 [axiom, in Coq.FSets.FSetInterface]
partition_1 [axiom, in Coq.FSets.FSetWeakInterface]
partition_2 [axiom, in Coq.FSets.FSetWeakInterface]
partition_2 [axiom, in Coq.FSets.FSetInterface]
PartSum [library]
pascal [lemma, in Coq.Reals.Binomial]
pascal_step1 [lemma, in Coq.Reals.Binomial]
pascal_step2 [lemma, in Coq.Reals.Binomial]
pascal_step3 [lemma, in Coq.Reals.Binomial]
Pbit [definition, in Coq.NArith.Ndigits]
Pcase [lemma, in Coq.NArith.BinPos]
Pcompare [definition, in Coq.NArith.BinPos]
Pcompare [definition, in Coq.Arith.Compare]
Pcompare_antisym [lemma, in Coq.NArith.BinPos]
Pcompare_Eq_eq [lemma, in Coq.NArith.BinPos]
Pcompare_Gt_Gt [lemma, in Coq.NArith.BinPos]
Pcompare_Gt_Lt [lemma, in Coq.NArith.BinPos]
Pcompare_Lt_Gt [lemma, in Coq.NArith.BinPos]
Pcompare_Lt_Lt [lemma, in Coq.NArith.BinPos]
Pcompare_minus_l [lemma, in Coq.NArith.Pnat]
Pcompare_minus_r [lemma, in Coq.NArith.Pnat]
Pcompare_not_Eq [lemma, in Coq.NArith.BinPos]
Pcompare_Peqb [lemma, in Coq.NArith.Ndec]
Pcompare_refl [lemma, in Coq.NArith.BinPos]
Pdiv2 [definition, in Coq.NArith.BinPos]
Pdiv2 [lemma, in Coq.ZArith.Zbinary]
Pdouble_mask [definition, in Coq.NArith.BinPos]
Pdouble_minus_one [definition, in Coq.NArith.BinPos]
Pdouble_minus_one_o_succ_eq_xI [lemma, in Coq.NArith.BinPos]
Pdouble_minus_two [definition, in Coq.NArith.BinPos]
Pdouble_plus_one_mask [definition, in Coq.NArith.BinPos]
Peano [library]
Peano_dec [library]
Peirce [lemma, in Coq.Logic.Classical_Prop]
Peqb [definition, in Coq.NArith.Ndec]
Peqb_correct [lemma, in Coq.NArith.Ndec]
Peqb_Pcompare [lemma, in Coq.NArith.Ndec]
peq_dec [lemma, in Coq.FSets.FMapPositive]
PER [inductive, in Coq.Sets.Relations_1]
PER [inductive, in Coq.Relations.Relation_Definitions]
Permut [library]
Permutation [inductive, in Coq.Lists.List]
permutation [definition, in Coq.Sorting.Permutation]
Permutation [library]
Permutation_app [lemma, in Coq.Lists.List]
Permutation_app_head [lemma, in Coq.Lists.List]
Permutation_app_inv [lemma, in Coq.Lists.List]
Permutation_app_inv_l [lemma, in Coq.Lists.List]
Permutation_app_inv_r [lemma, in Coq.Lists.List]
Permutation_app_swap [lemma, in Coq.Lists.List]
Permutation_app_tail [lemma, in Coq.Lists.List]
Permutation_cons_app [lemma, in Coq.Lists.List]
Permutation_cons_app_inv [lemma, in Coq.Lists.List]
Permutation_cons_inv [lemma, in Coq.Lists.List]
Permutation_in [lemma, in Coq.Lists.List]
Permutation_ind_bis [lemma, in Coq.Lists.List]
Permutation_length [lemma, in Coq.Lists.List]
permutation_map [lemma, in Coq.Sorting.PermutEq]
Permutation_map [lemma, in Coq.Lists.List]
Permutation_nil [lemma, in Coq.Lists.List]
Permutation_nil_cons [lemma, in Coq.Lists.List]
permutation_Permutation [lemma, in Coq.Sorting.PermutEq]
Permutation_refl [lemma, in Coq.Lists.List]
Permutation_rev [lemma, in Coq.Lists.List]
Permutation_sym [lemma, in Coq.Lists.List]
Permutation_trans [lemma, in Coq.Lists.List]
PermutEq [library]
PermutSetoid [library]
permut_add_cons_inside [lemma, in Coq.Sorting.Permutation]
permut_add_inside [lemma, in Coq.Sorting.Permutation]
permut_app [lemma, in Coq.Sorting.Permutation]
permut_app_inv1 [lemma, in Coq.Sorting.Permutation]
permut_app_inv2 [lemma, in Coq.Sorting.Permutation]
permut_cons [lemma, in Coq.Sorting.Permutation]
permut_cons_In [lemma, in Coq.Sorting.PermutEq]
permut_cons_InA [lemma, in Coq.Sorting.PermutSetoid]
permut_conv_inv [lemma, in Coq.Sorting.Permutation]
permut_InA_InA [lemma, in Coq.Sorting.PermutSetoid]
permut_In_In [lemma, in Coq.Sorting.PermutEq]
permut_length [lemma, in Coq.Sorting.PermutEq]
permut_length [lemma, in Coq.Sorting.PermutSetoid]
permut_length_1 [lemma, in Coq.Sorting.PermutEq]
permut_length_1 [lemma, in Coq.Sorting.PermutSetoid]
permut_length_2 [lemma, in Coq.Sorting.PermutSetoid]
permut_length_2 [lemma, in Coq.Sorting.PermutEq]
permut_map [lemma, in Coq.Sorting.PermutSetoid]
permut_middle [lemma, in Coq.Sorting.Permutation]
permut_nil [lemma, in Coq.Sorting.PermutSetoid]
permut_nil [lemma, in Coq.Sorting.PermutEq]
permut_refl [lemma, in Coq.Sorting.Permutation]
permut_remove_hd [lemma, in Coq.Sorting.Permutation]
permut_rev [lemma, in Coq.Sorting.Permutation]
permut_sym [lemma, in Coq.Sorting.Permutation]
permut_sym_app [lemma, in Coq.Sorting.Permutation]
permut_tran [lemma, in Coq.Sorting.Permutation]
perm_left [lemma, in Coq.Sets.Permut]
perm_nil [constructor, in Coq.Lists.List]
perm_right [lemma, in Coq.Sets.Permut]
perm_skip [constructor, in Coq.Lists.List]
perm_swap [constructor, in Coq.Lists.List]
perm_trans [constructor, in Coq.Lists.List]
Pgcd [definition, in Coq.ZArith.Znumtheory]
Pgcdn [definition, in Coq.ZArith.Znumtheory]
Pgcdn_correct [lemma, in Coq.ZArith.Znumtheory]
Pgcd_correct [lemma, in Coq.ZArith.Znumtheory]
Pggcd [definition, in Coq.ZArith.Znumtheory]
Pggcdn [definition, in Coq.ZArith.Znumtheory]
Pggcdn_correct_divisors [lemma, in Coq.ZArith.Znumtheory]
Pggcdn_gcdn [lemma, in Coq.ZArith.Znumtheory]
Pggcd_correct_divisors [lemma, in Coq.ZArith.Znumtheory]
Pggcd_gcd [lemma, in Coq.ZArith.Znumtheory]
phi_sequence [definition, in Coq.Reals.RiemannInt]
phi_sequence_prop [lemma, in Coq.Reals.RiemannInt]
PI [module, in Coq.Logic.ProofIrrelevance]
PI [definition, in Coq.Reals.AltSeries]
Pigeonhole [lemma, in Coq.Sets.Image]
Pigeonhole_bis [lemma, in Coq.Sets.Infinite_sets]
Pigeonhole_principle [lemma, in Coq.Sets.Image]
Pigeonhole_ter [lemma, in Coq.Sets.Infinite_sets]
Pind [lemma, in Coq.NArith.BinPos]
PI.proof_irrelevance [definition, in Coq.Logic.ProofIrrelevance]
PI2_RGT_0 [lemma, in Coq.Reals.Rtrigo]
PI2_Rlt_PI [lemma, in Coq.Reals.Rtrigo]
PI4_RGT_0 [lemma, in Coq.Reals.Rtrigo_calc]
PI4_RLT_PI2 [lemma, in Coq.Reals.Rtrigo]
PI6_RGT_0 [lemma, in Coq.Reals.Rtrigo_calc]
PI6_RLT_PI2 [lemma, in Coq.Reals.Rtrigo_calc]
PI_ineq [lemma, in Coq.Reals.AltSeries]
PI_neq0 [lemma, in Coq.Reals.Rtrigo]
PI_RGT_0 [lemma, in Coq.Reals.AltSeries]
PI_tg [definition, in Coq.Reals.AltSeries]
PI_tg_cv [lemma, in Coq.Reals.AltSeries]
PI_tg_decreasing [lemma, in Coq.Reals.AltSeries]
PI_tg_pos [lemma, in Coq.Reals.AltSeries]
PI_4 [lemma, in Coq.Reals.Rtrigo_alt]
plat [definition, in Coq.Reals.Rtrigo_calc]
plus [definition, in Coq.Init.Peano]
plus [axiom, in Coq.ZArith.Int]
Plus [library]
plus_acc [definition, in Coq.Arith.Plus]
plus_assoc [lemma, in Coq.Arith.Plus]
plus_assoc_reverse [lemma, in Coq.Arith.Plus]
plus_comm [lemma, in Coq.Arith.Plus]
plus_fct [definition, in Coq.Reals.Ranalysis1]
plus_frac_part1 [lemma, in Coq.Reals.R_Ifp]
plus_frac_part2 [lemma, in Coq.Reals.R_Ifp]
plus_gt_compat_l [lemma, in Coq.Arith.Gt]
plus_gt_reg_l [lemma, in Coq.Arith.Gt]
plus_INR [lemma, in Coq.Reals.RIneq]
plus_Int_part1 [lemma, in Coq.Reals.R_Ifp]
plus_Int_part2 [lemma, in Coq.Reals.R_Ifp]
plus_is_O [lemma, in Coq.Arith.Plus]
plus_is_one [definition, in Coq.Arith.Plus]
plus_iter [definition, in Coq.NArith.BinPos]
plus_iter_eq_plus [lemma, in Coq.NArith.BinPos]
plus_iter_xI [lemma, in Coq.NArith.BinPos]
plus_iter_xO [lemma, in Coq.NArith.BinPos]
plus_IZR [lemma, in Coq.Reals.RIneq]
plus_IZR_NEG_POS [lemma, in Coq.Reals.RIneq]
plus_le_compat [lemma, in Coq.Arith.Plus]
plus_le_compat_l [lemma, in Coq.Arith.Plus]
plus_le_compat_r [lemma, in Coq.Arith.Plus]
plus_le_is_le [lemma, in Coq.Reals.RIneq]
plus_le_lt_compat [lemma, in Coq.Arith.Plus]
plus_le_reg_l [lemma, in Coq.Arith.Plus]
plus_lt_compat [lemma, in Coq.Arith.Plus]
plus_lt_compat_l [lemma, in Coq.Arith.Plus]
plus_lt_compat_r [lemma, in Coq.Arith.Plus]
plus_lt_is_lt [lemma, in Coq.Reals.RIneq]
plus_lt_le_compat [lemma, in Coq.Arith.Plus]
plus_lt_reg_l [lemma, in Coq.Arith.Plus]
plus_minus [lemma, in Coq.Arith.Minus]
plus_n_O [lemma, in Coq.Init.Peano]
plus_n_Sm [lemma, in Coq.Init.Peano]
plus_O_n [lemma, in Coq.Init.Peano]
plus_permute [lemma, in Coq.Arith.Plus]
plus_permute_2_in_4 [lemma, in Coq.Arith.Plus]
plus_reg_l [lemma, in Coq.Arith.Plus]
plus_Snm_nSm [lemma, in Coq.Arith.Plus]
plus_Sn_m [lemma, in Coq.Init.Peano]
plus_sum [lemma, in Coq.Reals.PartSum]
plus_tail_plus [lemma, in Coq.Arith.Plus]
plus_0_l [lemma, in Coq.Arith.Plus]
plus_0_r [lemma, in Coq.Arith.Plus]
Pminus [definition, in Coq.NArith.BinPos]
Pminus_mask [definition, in Coq.NArith.BinPos]
Pminus_mask_carry [definition, in Coq.NArith.BinPos]
Pminus_mask_diag [lemma, in Coq.NArith.BinPos]
Pminus_mask_Gt [lemma, in Coq.NArith.BinPos]
Pminus_Zminus [lemma, in Coq.ZArith.Znumtheory]
Pmult [definition, in Coq.NArith.BinPos]
Pmult_assoc [lemma, in Coq.NArith.BinPos]
Pmult_comm [lemma, in Coq.NArith.BinPos]
Pmult_minus_distr_l [lemma, in Coq.NArith.Pnat]
Pmult_nat [definition, in Coq.NArith.BinPos]
Pmult_nat_l_plus_morphism [lemma, in Coq.NArith.Pnat]
Pmult_nat_mult_permute [lemma, in Coq.NArith.Pnat]
Pmult_nat_plus_carry_morphism [lemma, in Coq.NArith.Pnat]
Pmult_nat_r_plus_morphism [lemma, in Coq.NArith.Pnat]
Pmult_nat_succ_morphism [lemma, in Coq.NArith.Pnat]
Pmult_nat_2_mult_2_permute [lemma, in Coq.NArith.Pnat]
Pmult_nat_4_mult_2_permute [lemma, in Coq.NArith.Pnat]
Pmult_plus_distr_l [lemma, in Coq.NArith.BinPos]
Pmult_plus_distr_r [lemma, in Coq.NArith.BinPos]
Pmult_reg_l [lemma, in Coq.NArith.BinPos]
Pmult_reg_r [lemma, in Coq.NArith.BinPos]
Pmult_xI_mult_xO_discr [lemma, in Coq.NArith.BinPos]
Pmult_xI_permute_r [lemma, in Coq.NArith.BinPos]
Pmult_xO_discr [lemma, in Coq.NArith.BinPos]
Pmult_xO_permute_r [lemma, in Coq.NArith.BinPos]
Pmult_1_inversion_l [lemma, in Coq.NArith.BinPos]
Pmult_1_r [lemma, in Coq.NArith.BinPos]
Pnat [library]
PO [inductive, in Coq.Sets.Partial_Order]
point_adherent [definition, in Coq.Reals.Rtopology]
poly [lemma, in Coq.Reals.Rfunctions]
positive [inductive, in Coq.NArith.BinPos]
PositiveMap [module, in Coq.FSets.FMapPositive]
PositiveMapAdditionalFacts [module, in Coq.FSets.FMapPositive]
PositiveMapAdditionalFacts.gsident [lemma, in Coq.FSets.FMapPositive]
PositiveMapAdditionalFacts.gsspec [lemma, in Coq.FSets.FMapPositive]
PositiveMapAdditionalFacts.map2_commut [lemma, in Coq.FSets.FMapPositive]
PositiveMapAdditionalFacts.xmap2_lr [lemma, in Coq.FSets.FMapPositive]
PositiveMap.add [definition, in Coq.FSets.FMapPositive]
PositiveMap.add_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.add_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.add_3 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.elements [definition, in Coq.FSets.FMapPositive]
PositiveMap.elements_complete [lemma, in Coq.FSets.FMapPositive]
PositiveMap.elements_correct [lemma, in Coq.FSets.FMapPositive]
PositiveMap.elements_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.elements_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.elements_3 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.empty [definition, in Coq.FSets.FMapPositive]
PositiveMap.Empty [definition, in Coq.FSets.FMapPositive]
PositiveMap.Empty_alt [lemma, in Coq.FSets.FMapPositive]
PositiveMap.Empty_Node [lemma, in Coq.FSets.FMapPositive]
PositiveMap.empty_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.equal [definition, in Coq.FSets.FMapPositive]
PositiveMap.Equal [definition, in Coq.FSets.FMapPositive]
PositiveMap.equal_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.equal_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.eq_key [definition, in Coq.FSets.FMapPositive]
PositiveMap.eq_key_elt [definition, in Coq.FSets.FMapPositive]
PositiveMap.find [definition, in Coq.FSets.FMapPositive]
PositiveMap.find_xfind_h [lemma, in Coq.FSets.FMapPositive]
PositiveMap.find_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.find_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.fold [definition, in Coq.FSets.FMapPositive]
PositiveMap.fold_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.gempty [lemma, in Coq.FSets.FMapPositive]
PositiveMap.gleaf [lemma, in Coq.FSets.FMapPositive]
PositiveMap.gmapi [lemma, in Coq.FSets.FMapPositive]
PositiveMap.gmap2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.gro [lemma, in Coq.FSets.FMapPositive]
PositiveMap.grs [lemma, in Coq.FSets.FMapPositive]
PositiveMap.gso [lemma, in Coq.FSets.FMapPositive]
PositiveMap.gss [lemma, in Coq.FSets.FMapPositive]
PositiveMap.In [definition, in Coq.FSets.FMapPositive]
PositiveMap.is_empty [definition, in Coq.FSets.FMapPositive]
PositiveMap.is_empty_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.is_empty_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.key [definition, in Coq.FSets.FMapPositive]
PositiveMap.Leaf [constructor, in Coq.FSets.FMapPositive]
PositiveMap.lt_key [definition, in Coq.FSets.FMapPositive]
PositiveMap.map [definition, in Coq.FSets.FMapPositive]
PositiveMap.mapi [definition, in Coq.FSets.FMapPositive]
PositiveMap.mapi_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.mapi_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.MapsTo [definition, in Coq.FSets.FMapPositive]
PositiveMap.MapsTo_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.map2 [definition, in Coq.FSets.FMapPositive]
PositiveMap.map2_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.map2_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.map_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.map_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.mem [definition, in Coq.FSets.FMapPositive]
PositiveMap.mem_find [lemma, in Coq.FSets.FMapPositive]
PositiveMap.mem_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.mem_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.Node [constructor, in Coq.FSets.FMapPositive]
PositiveMap.None [definition, in Coq.FSets.FMapPositive]
PositiveMap.remove [definition, in Coq.FSets.FMapPositive]
PositiveMap.remove_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.remove_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.remove_3 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.rleaf [lemma, in Coq.FSets.FMapPositive]
PositiveMap.t [definition, in Coq.FSets.FMapPositive]
PositiveMap.tree [inductive, in Coq.FSets.FMapPositive]
PositiveMap.xelements [definition, in Coq.FSets.FMapPositive]
PositiveMap.xelements_bits_lt_1 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_bits_lt_2 [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_complete [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_correct [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_hi [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_ho [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_ih [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_ii [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_io [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_oh [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_oi [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_oo [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xelements_sort [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xfind [definition, in Coq.FSets.FMapPositive]
PositiveMap.xfind_left [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xgmapi [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xgmap2_l [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xgmap2_r [lemma, in Coq.FSets.FMapPositive]
PositiveMap.xmapi [definition, in Coq.FSets.FMapPositive]
PositiveMap.xmap2_l [definition, in Coq.FSets.FMapPositive]
PositiveMap.xmap2_r [definition, in Coq.FSets.FMapPositive]
PositiveMap._map2 [definition, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits [module, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.bits_lt [definition, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.bits_lt_antirefl [lemma, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.bits_lt_trans [lemma, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.compare [definition, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.eq [definition, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.eq_refl [lemma, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.eq_sym [lemma, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.eq_trans [lemma, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.lt [definition, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.lt_not_eq [lemma, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.lt_trans [lemma, in Coq.FSets.FMapPositive]
PositiveOrderedTypeBits.t [definition, in Coq.FSets.FMapPositive]
Positive_as_DT [module, in Coq.Logic.DecidableTypeEx]
Positive_as_OT [module, in Coq.FSets.OrderedTypeEx]
positive_derivative [lemma, in Coq.Reals.MVT]
positive_mask [inductive, in Coq.NArith.BinPos]
positivity_seq [definition, in Coq.Reals.AltSeries]
posreal [inductive, in Coq.Reals.RIneq]
pos_INR [lemma, in Coq.Reals.RIneq]
pos_Rl [definition, in Coq.Reals.RList]
pos_Rl_P1 [lemma, in Coq.Reals.RList]
pos_Rl_P2 [lemma, in Coq.Reals.RList]
pow [definition, in Coq.Reals.Rpow_def]
Pow [definition, in Coq.Relations.Relation_Operators]
pow [definition, in Coq.Logic.Berardi]
powerRZ [definition, in Coq.Reals.Rfunctions]
powerRZ_add [lemma, in Coq.Reals.Rfunctions]
powerRZ_le [lemma, in Coq.Reals.Rfunctions]
powerRZ_lt [lemma, in Coq.Reals.Rfunctions]
powerRZ_NOR [lemma, in Coq.Reals.Rfunctions]
powerRZ_O [lemma, in Coq.Reals.Rfunctions]
powerRZ_R1 [lemma, in Coq.Reals.Rfunctions]
powerRZ_1 [lemma, in Coq.Reals.Rfunctions]
Powerset [library]
Powerset_Classical_facts [library]
Powerset_facts [library]
Power_monotonic [lemma, in Coq.Reals.Rfunctions]
Power_set [inductive, in Coq.Sets.Powerset]
Power_set_Inhabited [lemma, in Coq.Sets.Powerset]
Power_set_PO [definition, in Coq.Sets.Powerset]
pow1 [lemma, in Coq.Reals.Rfunctions]
pow_add [lemma, in Coq.Reals.Rfunctions]
pow_fct [definition, in Coq.Reals.Ranalysis1]
pow_i [lemma, in Coq.Reals.Rtrigo_def]
pow_incr [lemma, in Coq.Reals.Rfunctions]
pow_IZR [lemma, in Coq.Reals.RIneq]
pow_le [lemma, in Coq.Reals.Rfunctions]
pow_lt [lemma, in Coq.Reals.Rfunctions]
pow_lt_1_zero [lemma, in Coq.Reals.Rfunctions]
pow_maj_Rabs [lemma, in Coq.Reals.Rfunctions]
pow_mult [lemma, in Coq.Reals.Rfunctions]
pow_ne_zero [lemma, in Coq.Reals.Rfunctions]
pow_nonzero [lemma, in Coq.Reals.Rfunctions]
pow_O [lemma, in Coq.Reals.Rfunctions]
pow_Rabs [lemma, in Coq.Reals.Rfunctions]
pow_RN_plus [lemma, in Coq.Reals.Rfunctions]
pow_Rsqr [lemma, in Coq.Reals.Rfunctions]
pow_R1 [lemma, in Coq.Reals.Rfunctions]
pow_R1_Rle [lemma, in Coq.Reals.Rfunctions]
pow_sqr [lemma, in Coq.Reals.Cos_rel]
Pow_x_infinity [lemma, in Coq.Reals.Rfunctions]
pow_1 [lemma, in Coq.Reals.Rfunctions]
pow_1_abs [lemma, in Coq.Reals.Rfunctions]
pow_1_even [lemma, in Coq.Reals.Rfunctions]
pow_1_odd [lemma, in Coq.Reals.Rfunctions]
pow_2_n [definition, in Coq.Reals.Rsqrt_def]
pow_2_n_growing [lemma, in Coq.Reals.Rsqrt_def]
pow_2_n_infty [lemma, in Coq.Reals.Rsqrt_def]
pow_2_n_neq_R0 [lemma, in Coq.Reals.Rsqrt_def]
Pplength [definition, in Coq.NArith.Ndist]
Pplus [definition, in Coq.NArith.BinPos]
Pplus_assoc [lemma, in Coq.NArith.BinPos]
Pplus_carry [definition, in Coq.NArith.BinPos]
Pplus_carry_no_neutral [lemma, in Coq.NArith.BinPos]
Pplus_carry_plus [lemma, in Coq.NArith.BinPos]
Pplus_carry_pred_eq_plus [lemma, in Coq.NArith.BinPos]
Pplus_carry_reg_l [lemma, in Coq.NArith.BinPos]
Pplus_carry_reg_r [lemma, in Coq.NArith.BinPos]
Pplus_carry_spec [lemma, in Coq.NArith.BinPos]
Pplus_comm [lemma, in Coq.NArith.BinPos]
Pplus_diag [lemma, in Coq.NArith.BinPos]
Pplus_minus [lemma, in Coq.NArith.BinPos]
Pplus_no_neutral [lemma, in Coq.NArith.BinPos]
Pplus_one_succ_l [lemma, in Coq.NArith.BinPos]
Pplus_one_succ_r [lemma, in Coq.NArith.BinPos]
Pplus_reg_l [lemma, in Coq.NArith.BinPos]
Pplus_reg_r [lemma, in Coq.NArith.BinPos]
Pplus_succ_permute_l [lemma, in Coq.NArith.BinPos]
Pplus_succ_permute_r [lemma, in Coq.NArith.BinPos]
Pplus_xI_double_minus_one [lemma, in Coq.NArith.BinPos]
Pplus_xO_double_minus_one [lemma, in Coq.NArith.BinPos]
Ppred [definition, in Coq.NArith.BinPos]
Ppred_succ [lemma, in Coq.NArith.BinPos]
Prec [definition, in Coq.NArith.BinPos]
pred [definition, in Coq.Init.Peano]
PredicateExtensionality [definition, in Coq.Logic.Diaconescu]
pred_ext_and_rel_choice_imp_EM [lemma, in Coq.Logic.Diaconescu]
pred_of_minus [lemma, in Coq.Arith.Minus]
pred_o_P_of_succ_nat_o_nat_of_P_eq_id [lemma, in Coq.NArith.Pnat]
pred_Sn [lemma, in Coq.Init.Peano]
prefix [definition, in Coq.Strings.String]
prefix_correct [lemma, in Coq.Strings.String]
Prelude [library]
Preorder [inductive, in Coq.Sets.Relations_1]
preorder [inductive, in Coq.Relations.Relation_Definitions]
prime [inductive, in Coq.ZArith.Znumtheory]
prime_divisors [lemma, in Coq.ZArith.Znumtheory]
prime_intro [constructor, in Coq.ZArith.Znumtheory]
prime_mult [lemma, in Coq.ZArith.Znumtheory]
prime_rel_prime [lemma, in Coq.ZArith.Znumtheory]
primitive [definition, in Coq.Reals.RiemannInt]
prod [inductive, in Coq.Init.Datatypes]
product_of_arguments [definition, in Coq.Setoids.Setoid]
prod_curry [definition, in Coq.Init.Datatypes]
prod_f_SO [definition, in Coq.Reals.Rprod]
prod_length [lemma, in Coq.Lists.List]
prod_neq_R0 [lemma, in Coq.Reals.RIneq]
prod_SO_pos [lemma, in Coq.Reals.Rprod]
prod_SO_Rle [lemma, in Coq.Reals.Rprod]
prod_SO_split [lemma, in Coq.Reals.Rprod]
prod_uncurry [definition, in Coq.Init.Datatypes]
projT1 [definition, in Coq.Init.Specif]
projT1_injective [lemma, in Coq.Logic.Diaconescu]
projT2 [definition, in Coq.Init.Specif]
proj1 [lemma, in Coq.Init.Logic]
proj1_inf [definition, in Coq.Logic.ChoiceFacts]
proj1_sig [definition, in Coq.Init.Specif]
proj2 [lemma, in Coq.Init.Logic]
proj2_sig [definition, in Coq.Init.Specif]
prolongement_C0 [lemma, in Coq.Reals.Rtopology]
ProofIrrelevance [module, in Coq.Logic.ProofIrrelevanceFacts]
ProofIrrelevance [definition, in Coq.Logic.ChoiceFacts]
ProofIrrelevance [library]
ProofIrrelevanceFacts [library]
ProofIrrelevanceTheory [module, in Coq.Logic.ProofIrrelevanceFacts]
ProofIrrelevanceTheory.Eq_rect_eq.eq_rect_eq [lemma, in Coq.Logic.ProofIrrelevanceFacts]
ProofIrrelevanceTheory.subsetT_eq_compat [lemma, in Coq.Logic.ProofIrrelevanceFacts]
ProofIrrelevanceTheory.subset_eq_compat [lemma, in Coq.Logic.ProofIrrelevanceFacts]
proof_irrel [lemma, in Coq.Logic.Diaconescu]
proof_irrelevance [definition, in Coq.Logic.ClassicalFacts]
proof_irrelevance [axiom, in Coq.Logic.ProofIrrelevance]
proof_irrelevance [lemma, in Coq.Logic.Classical_Prop]
proof_irrelevance [axiom, in Coq.Logic.ProofIrrelevanceFacts]
proof_irrelevance_cc [lemma, in Coq.Logic.ClassicalFacts]
proof_irrelevance_cci [lemma, in Coq.Logic.ClassicalFacts]
proof_irrel_rel_choice_imp_eq_dec [lemma, in Coq.Logic.Diaconescu]
proof_irrel_rel_choice_imp_eq_dec' [lemma, in Coq.Logic.Diaconescu]
ProperElementToKeep [constructor, in Coq.Setoids.Setoid]
Properties [module, in Coq.FSets.FSetWeakProperties]
Properties [module, in Coq.FSets.FSetProperties]
Properties.Add [definition, in Coq.FSets.FSetWeakProperties]
Properties.Add [definition, in Coq.FSets.FSetProperties]
Properties.Add_add [lemma, in Coq.FSets.FSetWeakProperties]
Properties.Add_add [lemma, in Coq.FSets.FSetProperties]
Properties.add_add [lemma, in Coq.FSets.FSetProperties]
Properties.add_add [lemma, in Coq.FSets.FSetWeakProperties]
Properties.add_cardinal_1 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.add_cardinal_1 [lemma, in Coq.FSets.FSetProperties]
Properties.add_cardinal_2 [lemma, in Coq.FSets.FSetProperties]
Properties.add_cardinal_2 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.add_equal [lemma, in Coq.FSets.FSetProperties]
Properties.add_equal [lemma, in Coq.FSets.FSetWeakProperties]
Properties.add_fold [lemma, in Coq.FSets.FSetWeakProperties]
Properties.add_fold [lemma, in Coq.FSets.FSetProperties]
Properties.Add_remove [lemma, in Coq.FSets.FSetProperties]
Properties.add_remove [lemma, in Coq.FSets.FSetProperties]
Properties.Add_remove [lemma, in Coq.FSets.FSetWeakProperties]
Properties.add_remove [lemma, in Coq.FSets.FSetWeakProperties]
Properties.add_union_singleton [lemma, in Coq.FSets.FSetWeakProperties]
Properties.add_union_singleton [lemma, in Coq.FSets.FSetProperties]
Properties.cardinal_fold [lemma, in Coq.FSets.FSetWeakProperties]
Properties.cardinal_fold [lemma, in Coq.FSets.FSetProperties]
Properties.cardinal_induction [lemma, in Coq.FSets.FSetProperties]
Properties.cardinal_induction [lemma, in Coq.FSets.FSetWeakProperties]
Properties.cardinal_inv_1 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.cardinal_inv_1 [lemma, in Coq.FSets.FSetProperties]
Properties.cardinal_inv_2 [lemma, in Coq.FSets.FSetProperties]
Properties.cardinal_inv_2 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.cardinal_0 [lemma, in Coq.FSets.FSetProperties]
Properties.cardinal_0 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.cardinal_1 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.cardinal_1 [lemma, in Coq.FSets.FSetProperties]
Properties.cardinal_2 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.cardinal_2 [lemma, in Coq.FSets.FSetProperties]
Properties.diff_inter_all [lemma, in Coq.FSets.FSetWeakProperties]
Properties.diff_inter_all [lemma, in Coq.FSets.FSetProperties]
Properties.diff_inter_cardinal [lemma, in Coq.FSets.FSetProperties]
Properties.diff_inter_cardinal [lemma, in Coq.FSets.FSetWeakProperties]
Properties.diff_inter_empty [lemma, in Coq.FSets.FSetWeakProperties]
Properties.diff_inter_empty [lemma, in Coq.FSets.FSetProperties]
Properties.diff_subset [lemma, in Coq.FSets.FSetWeakProperties]
Properties.diff_subset [lemma, in Coq.FSets.FSetProperties]
Properties.diff_subset_equal [lemma, in Coq.FSets.FSetProperties]
Properties.diff_subset_equal [lemma, in Coq.FSets.FSetWeakProperties]
Properties.double_inclusion [lemma, in Coq.FSets.FSetWeakProperties]
Properties.double_inclusion [lemma, in Coq.FSets.FSetProperties]
Properties.empty_cardinal [lemma, in Coq.FSets.FSetWeakProperties]
Properties.empty_cardinal [lemma, in Coq.FSets.FSetProperties]
Properties.empty_diff_1 [lemma, in Coq.FSets.FSetProperties]
Properties.empty_diff_1 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.empty_diff_2 [lemma, in Coq.FSets.FSetProperties]
Properties.empty_diff_2 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.empty_inter_1 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.empty_inter_1 [lemma, in Coq.FSets.FSetProperties]
Properties.empty_inter_2 [lemma, in Coq.FSets.FSetProperties]
Properties.empty_inter_2 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.empty_is_empty_1 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.empty_is_empty_1 [lemma, in Coq.FSets.FSetProperties]
Properties.empty_is_empty_2 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.empty_is_empty_2 [lemma, in Coq.FSets.FSetProperties]
Properties.empty_union_1 [lemma, in Coq.FSets.FSetProperties]
Properties.empty_union_1 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.empty_union_2 [lemma, in Coq.FSets.FSetProperties]
Properties.empty_union_2 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.Equal_cardinal [lemma, in Coq.FSets.FSetProperties]
Properties.Equal_cardinal [lemma, in Coq.FSets.FSetWeakProperties]
Properties.Equal_cardinal_aux [lemma, in Coq.FSets.FSetWeakProperties]
Properties.Equal_cardinal_aux [lemma, in Coq.FSets.FSetProperties]
Properties.equal_refl [lemma, in Coq.FSets.FSetWeakProperties]
Properties.equal_refl [lemma, in Coq.FSets.FSetProperties]
Properties.Equal_remove [lemma, in Coq.FSets.FSetWeakProperties]
Properties.Equal_remove [lemma, in Coq.FSets.FSetProperties]
Properties.equal_sym [lemma, in Coq.FSets.FSetProperties]
Properties.equal_sym [lemma, in Coq.FSets.FSetWeakProperties]
Properties.equal_trans [lemma, in Coq.FSets.FSetWeakProperties]
Properties.equal_trans [lemma, in Coq.FSets.FSetProperties]
Properties.fold_add [lemma, in Coq.FSets.FSetWeakProperties]
Properties.fold_add [lemma, in Coq.FSets.FSetProperties]
Properties.fold_commutes [lemma, in Coq.FSets.FSetProperties]
Properties.fold_commutes [lemma, in Coq.FSets.FSetWeakProperties]
Properties.fold_diff_inter [lemma, in Coq.FSets.FSetWeakProperties]
Properties.fold_diff_inter [lemma, in Coq.FSets.FSetProperties]
Properties.fold_empty [lemma, in Coq.FSets.FSetWeakProperties]
Properties.fold_empty [lemma, in Coq.FSets.FSetProperties]
Properties.fold_equal [lemma, in Coq.FSets.FSetWeakProperties]
Properties.fold_equal [lemma, in Coq.FSets.FSetProperties]
Properties.fold_init [lemma, in Coq.FSets.FSetProperties]
Properties.fold_init [lemma, in Coq.FSets.FSetWeakProperties]
Properties.fold_plus [lemma, in Coq.FSets.FSetWeakProperties]
Properties.fold_plus [lemma, in Coq.FSets.FSetProperties]
Properties.fold_union [lemma, in Coq.FSets.FSetWeakProperties]
Properties.fold_union [lemma, in Coq.FSets.FSetProperties]
Properties.fold_union_inter [lemma, in Coq.FSets.FSetProperties]
Properties.fold_union_inter [lemma, in Coq.FSets.FSetWeakProperties]
Properties.fold_0 [lemma, in Coq.FSets.FSetProperties]
Properties.fold_0 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.fold_1 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.fold_1 [lemma, in Coq.FSets.FSetProperties]
Properties.fold_2 [lemma, in Coq.FSets.FSetProperties]
Properties.fold_2 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.inter_Add [lemma, in Coq.FSets.FSetProperties]
Properties.inter_Add [lemma, in Coq.FSets.FSetWeakProperties]
Properties.inter_add_1 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.inter_add_1 [lemma, in Coq.FSets.FSetProperties]
Properties.inter_add_2 [lemma, in Coq.FSets.FSetProperties]
Properties.inter_Add_2 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.inter_Add_2 [lemma, in Coq.FSets.FSetProperties]
Properties.inter_add_2 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.inter_assoc [lemma, in Coq.FSets.FSetWeakProperties]
Properties.inter_assoc [lemma, in Coq.FSets.FSetProperties]
Properties.inter_equal_1 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.inter_equal_1 [lemma, in Coq.FSets.FSetProperties]
Properties.inter_equal_2 [lemma, in Coq.FSets.FSetProperties]
Properties.inter_equal_2 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.inter_subset_equal [lemma, in Coq.FSets.FSetProperties]
Properties.inter_subset_equal [lemma, in Coq.FSets.FSetWeakProperties]
Properties.inter_subset_1 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.inter_subset_1 [lemma, in Coq.FSets.FSetProperties]
Properties.inter_subset_2 [lemma, in Coq.FSets.FSetProperties]
Properties.inter_subset_2 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.inter_subset_3 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.inter_subset_3 [lemma, in Coq.FSets.FSetProperties]
Properties.inter_sym [lemma, in Coq.FSets.FSetWeakProperties]
Properties.inter_sym [lemma, in Coq.FSets.FSetProperties]
Properties.In_dec [lemma, in Coq.FSets.FSetProperties]
Properties.In_dec [lemma, in Coq.FSets.FSetWeakProperties]
Properties.in_subset [lemma, in Coq.FSets.FSetProperties]
Properties.in_subset [lemma, in Coq.FSets.FSetWeakProperties]
Properties.not_in_union [lemma, in Coq.FSets.FSetWeakProperties]
Properties.not_in_union [lemma, in Coq.FSets.FSetProperties]
Properties.remove_add [lemma, in Coq.FSets.FSetWeakProperties]
Properties.remove_add [lemma, in Coq.FSets.FSetProperties]
Properties.remove_cardinal_1 [lemma, in Coq.FSets.FSetProperties]
Properties.remove_cardinal_1 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.remove_cardinal_2 [lemma, in Coq.FSets.FSetProperties]
Properties.remove_cardinal_2 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.remove_diff_singleton [lemma, in Coq.FSets.FSetWeakProperties]
Properties.remove_diff_singleton [lemma, in Coq.FSets.FSetProperties]
Properties.remove_equal [lemma, in Coq.FSets.FSetWeakProperties]
Properties.remove_equal [lemma, in Coq.FSets.FSetProperties]
Properties.remove_fold_1 [lemma, in Coq.FSets.FSetProperties]
Properties.remove_fold_1 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.remove_fold_2 [lemma, in Coq.FSets.FSetProperties]
Properties.remove_fold_2 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.set_induction [lemma, in Coq.FSets.FSetWeakProperties]
Properties.set_induction [lemma, in Coq.FSets.FSetProperties]
Properties.singleton_cardinal [lemma, in Coq.FSets.FSetWeakProperties]
Properties.singleton_cardinal [lemma, in Coq.FSets.FSetProperties]
Properties.singleton_equal_add [lemma, in Coq.FSets.FSetWeakProperties]
Properties.singleton_equal_add [lemma, in Coq.FSets.FSetProperties]
Properties.subset_add_2 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.subset_add_2 [lemma, in Coq.FSets.FSetProperties]
Properties.subset_add_3 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.subset_add_3 [lemma, in Coq.FSets.FSetProperties]
Properties.subset_antisym [lemma, in Coq.FSets.FSetWeakProperties]
Properties.subset_antisym [lemma, in Coq.FSets.FSetProperties]
Properties.subset_cardinal [lemma, in Coq.FSets.FSetWeakProperties]
Properties.subset_cardinal [lemma, in Coq.FSets.FSetProperties]
Properties.subset_cardinal_lt [lemma, in Coq.FSets.FSetWeakProperties]
Properties.subset_cardinal_lt [lemma, in Coq.FSets.FSetProperties]
Properties.subset_diff [lemma, in Coq.FSets.FSetProperties]
Properties.subset_diff [lemma, in Coq.FSets.FSetWeakProperties]
Properties.subset_empty [lemma, in Coq.FSets.FSetProperties]
Properties.subset_empty [lemma, in Coq.FSets.FSetWeakProperties]
Properties.subset_equal [lemma, in Coq.FSets.FSetProperties]
Properties.subset_equal [lemma, in Coq.FSets.FSetWeakProperties]
Properties.subset_refl [lemma, in Coq.FSets.FSetProperties]
Properties.subset_refl [lemma, in Coq.FSets.FSetWeakProperties]
Properties.subset_remove_3 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.subset_remove_3 [lemma, in Coq.FSets.FSetProperties]
Properties.subset_trans [lemma, in Coq.FSets.FSetProperties]
Properties.subset_trans [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_Add [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_Add [lemma, in Coq.FSets.FSetProperties]
Properties.union_add [lemma, in Coq.FSets.FSetProperties]
Properties.union_add [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_assoc [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_assoc [lemma, in Coq.FSets.FSetProperties]
Properties.union_cardinal [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_cardinal [lemma, in Coq.FSets.FSetProperties]
Properties.union_cardinal_inter [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_cardinal_inter [lemma, in Coq.FSets.FSetProperties]
Properties.union_cardinal_le [lemma, in Coq.FSets.FSetProperties]
Properties.union_cardinal_le [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_Equal [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_Equal [lemma, in Coq.FSets.FSetProperties]
Properties.union_equal_1 [lemma, in Coq.FSets.FSetProperties]
Properties.union_equal_1 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_equal_2 [lemma, in Coq.FSets.FSetProperties]
Properties.union_equal_2 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_inter_cardinal [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_inter_cardinal [lemma, in Coq.FSets.FSetProperties]
Properties.union_inter_1 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_inter_1 [lemma, in Coq.FSets.FSetProperties]
Properties.union_inter_2 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_inter_2 [lemma, in Coq.FSets.FSetProperties]
Properties.union_subset_equal [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_subset_equal [lemma, in Coq.FSets.FSetProperties]
Properties.union_subset_1 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_subset_1 [lemma, in Coq.FSets.FSetProperties]
Properties.union_subset_2 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_subset_2 [lemma, in Coq.FSets.FSetProperties]
Properties.union_subset_3 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_subset_3 [lemma, in Coq.FSets.FSetProperties]
Properties.union_subset_4 [lemma, in Coq.FSets.FSetProperties]
Properties.union_subset_4 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_subset_5 [lemma, in Coq.FSets.FSetProperties]
Properties.union_subset_5 [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_sym [lemma, in Coq.FSets.FSetWeakProperties]
Properties.union_sym [lemma, in Coq.FSets.FSetProperties]
prop_degeneracy [definition, in Coq.Logic.ClassicalFacts]
prop_degen_em [lemma, in Coq.Logic.ClassicalFacts]
prop_degen_ext [lemma, in Coq.Logic.ClassicalFacts]
prop_eps [lemma, in Coq.Reals.Rlimit]
prop_ext [lemma, in Coq.Logic.Diaconescu]
prop_extensionality [definition, in Coq.Logic.ClassicalFacts]
prop_ext_A_eq_A_imp_A [lemma, in Coq.Logic.ClassicalFacts]
prop_ext_em_degen [lemma, in Coq.Logic.ClassicalFacts]
prop_ext_retract_A_A_imp_A [lemma, in Coq.Logic.ClassicalFacts]
pr_nu [lemma, in Coq.Reals.Ranalysis1]
pr_nu_var [lemma, in Coq.Reals.Ranalysis4]
pr_nu_var2 [lemma, in Coq.Reals.Ranalysis4]
Pser [definition, in Coq.Reals.Rseries]
PSeries_reg [library]
Psize [definition, in Coq.NArith.Ndigits]
Psize_monotone [lemma, in Coq.ZArith.Znumtheory]
Psucc [definition, in Coq.NArith.BinPos]
Psucc_discr [lemma, in Coq.NArith.BinPos]
Psucc_inj [lemma, in Coq.NArith.BinPos]
Psucc_not_one [lemma, in Coq.NArith.BinPos]
Psucc_o_double_minus_one_eq_xO [lemma, in Coq.NArith.BinPos]
Psucc_pred [lemma, in Coq.NArith.BinPos]
Pxor [definition, in Coq.NArith.Ndigits]
P' [definition, in Coq.Logic.ConstructiveEpsilon]
P'_decidable [lemma, in Coq.Logic.ConstructiveEpsilon]
p2b [definition, in Coq.Logic.ClassicalFacts]
P2Bv [definition, in Coq.NArith.Ndigits]
p2p1 [lemma, in Coq.Logic.ClassicalFacts]
p2p2 [lemma, in Coq.Logic.ClassicalFacts]
P_eventually_implies_acc [lemma, in Coq.Logic.ConstructiveEpsilon]
P_implies_acc [lemma, in Coq.Logic.ConstructiveEpsilon]
P_nth [inductive, in Coq.Arith.Between]
P_of_succ_nat [definition, in Coq.NArith.BinPos]
P_of_succ_nat_o_nat_of_P_eq_succ [lemma, in Coq.NArith.Pnat]
P_Rmin [lemma, in Coq.Reals.Rpower]

Global Index

(7984 entries)

Axiom Index

B

H

K

Q

V

W

X

Y

(401 entries)

Lemma Index

Y

(5228 entries)

Constructor Index

K

Q

W

Y

_

(292 entries)

Inductive Index

K

Y

_

(184 entries)

Definition Index

J

_

(1519 entries)

Module Index

A

B

C

G

H

J

L

Q

T

V

W

X

Y

_

(85 entries)

Library Index

K

V

X

Y

_

(275 entries)