| 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 | (26071 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 | (1003 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 | (815 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 | (1771 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 | (589 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 | (961 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 | (12021 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 | (508 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 | (308 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 | (479 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 | (496 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 | (906 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 | (1204 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 | (4844 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 | (166 entries) |
P (definition)
Padd [in Stdlib.setoid_ring.Ncring_polynom]padd [in Stdlib.micromega.ZMicromega]
padd [in Stdlib.micromega.RingMicromega]
Padd [in Stdlib.micromega.EnvRing]
Padd [in Stdlib.setoid_ring.Ring_polynom]
paddC [in Stdlib.micromega.RingMicromega]
PaddC [in Stdlib.micromega.EnvRing]
PaddC [in Stdlib.setoid_ring.Ring_polynom]
PaddCl [in Stdlib.setoid_ring.Ncring_polynom]
PaddC_ok [in Stdlib.micromega.RingMicromega]
PaddI [in Stdlib.micromega.EnvRing]
PaddI [in Stdlib.setoid_ring.Ring_polynom]
PaddX [in Stdlib.setoid_ring.Ncring_polynom]
PaddX [in Stdlib.micromega.EnvRing]
PaddX [in Stdlib.setoid_ring.Ring_polynom]
PairDecidableType.eq [in Stdlib.Structures.DecidableTypeEx]
PairDecidableType.eq [in Stdlib.Structures.EqualitiesFacts]
PairDecidableType.eq_dec [in Stdlib.Structures.DecidableTypeEx]
PairDecidableType.eq_dec [in Stdlib.Structures.EqualitiesFacts]
PairDecidableType.t [in Stdlib.Structures.DecidableTypeEx]
PairDecidableType.t [in Stdlib.Structures.EqualitiesFacts]
PairOrderedType.compare [in Stdlib.Structures.OrdersEx]
PairOrderedType.compare [in Stdlib.Structures.OrderedTypeEx]
PairOrderedType.eq [in Stdlib.Structures.OrderedTypeEx]
PairOrderedType.eq_dec [in Stdlib.Structures.OrderedTypeEx]
PairOrderedType.lt [in Stdlib.Structures.OrdersEx]
PairOrderedType.lt [in Stdlib.Structures.OrderedTypeEx]
PairOrderedType.t [in Stdlib.Structures.OrderedTypeEx]
PairUsualDecidableType.eq [in Stdlib.Structures.DecidableTypeEx]
PairUsualDecidableType.eq [in Stdlib.Structures.EqualitiesFacts]
PairUsualDecidableType.eq_dec [in Stdlib.Structures.DecidableTypeEx]
PairUsualDecidableType.eq_trans [in Stdlib.Structures.DecidableTypeEx]
PairUsualDecidableType.eq_sym [in Stdlib.Structures.DecidableTypeEx]
PairUsualDecidableType.eq_refl [in Stdlib.Structures.DecidableTypeEx]
PairUsualDecidableType.eq_dec [in Stdlib.Structures.EqualitiesFacts]
PairUsualDecidableType.t [in Stdlib.Structures.DecidableTypeEx]
PairUsualDecidableType.t [in Stdlib.Structures.EqualitiesFacts]
pair_of_and [in Stdlib.ssr.ssrfun]
parser [in Stdlib.Numbers.Cyclic.Int63.Sint63]
parser [in Stdlib.Floats.PrimFloat]
parser [in Stdlib.Numbers.Cyclic.Int63.PrimInt63]
partition [in Stdlib.Lists.List]
pcancel [in Stdlib.ssr.ssrfun]
pcomp [in Stdlib.ssr.ssrfun]
Pcompare [in Stdlib.Arith.Compare]
PCond [in Stdlib.setoid_ring.Field_theory]
Pcond_simpl_complete [in Stdlib.setoid_ring.Field_theory]
Pcond_simpl_gen [in Stdlib.setoid_ring.Field_theory]
Pdigits [in Stdlib.Numbers.Cyclic.Int63.Cyclic63]
Pdiv_eucl_correct [in Stdlib.NArith.Ndiv_def]
Pdiv_eucl [in Stdlib.NArith.Ndiv_def]
PEeval [in Stdlib.setoid_ring.Ncring_polynom]
PEeval [in Stdlib.micromega.EnvRing]
PEeval [in Stdlib.setoid_ring.Ring_polynom]
PEevalR [in Stdlib.nsatz.NsatzTactic]
Peq [in Stdlib.setoid_ring.Ncring_polynom]
Peq [in Stdlib.micromega.EnvRing]
Peq [in Stdlib.setoid_ring.Ring_polynom]
pequiv [in Stdlib.Classes.CEquivalence]
Pequiv [in Stdlib.setoid_ring.Ring_polynom]
pequiv [in Stdlib.Classes.Equivalence]
permutation [in Stdlib.Sorting.PermutSetoid]
PermutationA_sind [in Stdlib.Lists.SetoidPermutation]
PermutationA_ind [in Stdlib.Lists.SetoidPermutation]
Permutation_transp_sind [in Stdlib.Sorting.Permutation]
Permutation_transp_ind [in Stdlib.Sorting.Permutation]
Permutation_sind [in Stdlib.Sorting.Permutation]
Permutation_ind [in Stdlib.Sorting.Permutation]
PER_sind [in Stdlib.Sets.Relations_1]
PER_rec [in Stdlib.Sets.Relations_1]
PER_ind [in Stdlib.Sets.Relations_1]
PER_rect [in Stdlib.Sets.Relations_1]
PEsimp [in Stdlib.setoid_ring.Field_theory]
pexpr_times_nformula [in Stdlib.micromega.RingMicromega]
PExpr_sind [in Stdlib.micromega.EnvRing]
PExpr_rec [in Stdlib.micromega.EnvRing]
PExpr_ind [in Stdlib.micromega.EnvRing]
PExpr_rect [in Stdlib.micromega.EnvRing]
PExpr_eq [in Stdlib.setoid_ring.Field_theory]
PExpr_sind [in Stdlib.setoid_ring.Ring_polynom]
PExpr_rec [in Stdlib.setoid_ring.Ring_polynom]
PExpr_ind [in Stdlib.setoid_ring.Ring_polynom]
PExpr_rect [in Stdlib.setoid_ring.Ring_polynom]
PEZ [in Stdlib.nsatz.NsatzTactic]
phant_id [in Stdlib.ssr.ssrfun]
PhiR [in Stdlib.nsatz.NsatzTactic]
phi_sequence [in Stdlib.Reals.RiemannInt]
PI [in Stdlib.Reals.Rtrigo1]
PI_2_3_7_tg [in Stdlib.Reals.Machin]
PI_2_aux [in Stdlib.Reals.Rtrigo1]
PI_tg [in Stdlib.Reals.AltSeries]
PI.proof_irrelevance [in Stdlib.Logic.ProofIrrelevance]
PI2 [in Stdlib.Reals.Rtrigo1]
plat [in Stdlib.Reals.Rtrigo_calc]
plus_fct [in Stdlib.Reals.Ranalysis1]
plus_minus_stt [in Stdlib.Arith.Arith_base]
plus_assoc_reverse_stt [in Stdlib.Arith.Arith_base]
plus_gt_compat_l_stt [in Stdlib.Arith.Arith_base]
Pmul [in Stdlib.setoid_ring.Ncring_polynom]
pmul [in Stdlib.micromega.ZMicromega]
pmul [in Stdlib.micromega.RingMicromega]
Pmul [in Stdlib.micromega.EnvRing]
Pmul [in Stdlib.setoid_ring.Ring_polynom]
PmulC [in Stdlib.setoid_ring.Ncring_polynom]
PmulC [in Stdlib.micromega.EnvRing]
PmulC [in Stdlib.setoid_ring.Ring_polynom]
PmulC_aux [in Stdlib.setoid_ring.Ncring_polynom]
PmulC_aux [in Stdlib.micromega.EnvRing]
PmulC_aux [in Stdlib.setoid_ring.Ring_polynom]
PmulI [in Stdlib.micromega.EnvRing]
PmulI [in Stdlib.setoid_ring.Ring_polynom]
PNSubst [in Stdlib.micromega.EnvRing]
PNSubst [in Stdlib.setoid_ring.Ring_polynom]
PNSubstL [in Stdlib.micromega.EnvRing]
PNSubstL [in Stdlib.setoid_ring.Ring_polynom]
PNSubst1 [in Stdlib.micromega.EnvRing]
PNSubst1 [in Stdlib.setoid_ring.Ring_polynom]
pointwise_lifting [in Stdlib.Classes.RelationClasses]
pointwise_extension [in Stdlib.Classes.RelationClasses]
pointwise_relation [in Stdlib.Classes.Morphisms]
pointwise_relation [in Stdlib.Classes.CMorphisms]
point_in_holed_interval [in Stdlib.Reals.Runcountable]
point_adherent [in Stdlib.Reals.Rtopology]
PolC [in Stdlib.micromega.RingMicromega]
PolEnv [in Stdlib.micromega.RingMicromega]
poly_of_formula [in Stdlib.btauto.Reflect]
poly_mul [in Stdlib.btauto.Algebra]
poly_mul_mon [in Stdlib.btauto.Algebra]
poly_mul_cst [in Stdlib.btauto.Algebra]
poly_add [in Stdlib.btauto.Algebra]
poly_sind [in Stdlib.btauto.Algebra]
poly_rec [in Stdlib.btauto.Algebra]
poly_ind [in Stdlib.btauto.Algebra]
poly_rect [in Stdlib.btauto.Algebra]
PolZ [in Stdlib.nsatz.NsatzTactic]
PolZadd [in Stdlib.nsatz.NsatzTactic]
PolZeq [in Stdlib.nsatz.NsatzTactic]
PolZmul [in Stdlib.nsatz.NsatzTactic]
Pol_sind [in Stdlib.setoid_ring.Ncring_polynom]
Pol_rec [in Stdlib.setoid_ring.Ncring_polynom]
Pol_ind [in Stdlib.setoid_ring.Ncring_polynom]
Pol_rect [in Stdlib.setoid_ring.Ncring_polynom]
Pol_sind [in Stdlib.micromega.EnvRing]
Pol_rec [in Stdlib.micromega.EnvRing]
Pol_ind [in Stdlib.micromega.EnvRing]
Pol_rect [in Stdlib.micromega.EnvRing]
Pol_sind [in Stdlib.setoid_ring.Ring_polynom]
Pol_rec [in Stdlib.setoid_ring.Ring_polynom]
Pol_ind [in Stdlib.setoid_ring.Ring_polynom]
Pol_rect [in Stdlib.setoid_ring.Ring_polynom]
POneSubst [in Stdlib.micromega.EnvRing]
POneSubst [in Stdlib.setoid_ring.Ring_polynom]
Popp [in Stdlib.setoid_ring.Ncring_polynom]
popp [in Stdlib.micromega.ZMicromega]
popp [in Stdlib.micromega.RingMicromega]
Popp [in Stdlib.micromega.EnvRing]
Popp [in Stdlib.setoid_ring.Ring_polynom]
Poption_sind [in Stdlib.rtauto.Bintree]
Poption_rec [in Stdlib.rtauto.Bintree]
Poption_ind [in Stdlib.rtauto.Bintree]
Poption_rect [in Stdlib.rtauto.Bintree]
PositiveMap.add [in Stdlib.FSets.FMapPositive]
PositiveMap.cardinal [in Stdlib.FSets.FMapPositive]
PositiveMap.elements [in Stdlib.FSets.FMapPositive]
PositiveMap.Empty [in Stdlib.FSets.FMapPositive]
PositiveMap.empty [in Stdlib.FSets.FMapPositive]
PositiveMap.Equal [in Stdlib.FSets.FMapPositive]
PositiveMap.equal [in Stdlib.FSets.FMapPositive]
PositiveMap.Equiv [in Stdlib.FSets.FMapPositive]
PositiveMap.Equivb [in Stdlib.FSets.FMapPositive]
PositiveMap.eq_key_elt [in Stdlib.FSets.FMapPositive]
PositiveMap.eq_key [in Stdlib.FSets.FMapPositive]
PositiveMap.find [in Stdlib.FSets.FMapPositive]
PositiveMap.fold [in Stdlib.FSets.FMapPositive]
PositiveMap.In [in Stdlib.FSets.FMapPositive]
PositiveMap.is_empty [in Stdlib.FSets.FMapPositive]
PositiveMap.key [in Stdlib.FSets.FMapPositive]
PositiveMap.lt_key [in Stdlib.FSets.FMapPositive]
PositiveMap.map [in Stdlib.FSets.FMapPositive]
PositiveMap.mapi [in Stdlib.FSets.FMapPositive]
PositiveMap.MapsTo [in Stdlib.FSets.FMapPositive]
PositiveMap.map2 [in Stdlib.FSets.FMapPositive]
PositiveMap.mem [in Stdlib.FSets.FMapPositive]
PositiveMap.remove [in Stdlib.FSets.FMapPositive]
PositiveMap.t [in Stdlib.FSets.FMapPositive]
PositiveMap.tree_ind [in Stdlib.FSets.FMapPositive]
PositiveMap.xelements [in Stdlib.FSets.FMapPositive]
PositiveMap.xfind [in Stdlib.FSets.FMapPositive]
PositiveMap.xfoldi [in Stdlib.FSets.FMapPositive]
PositiveMap.xmapi [in Stdlib.FSets.FMapPositive]
PositiveMap.xmap2_r [in Stdlib.FSets.FMapPositive]
PositiveMap.xmap2_l [in Stdlib.FSets.FMapPositive]
PositiveMap._map2 [in Stdlib.FSets.FMapPositive]
PositiveOrderedTypeBits.bits_lt [in Stdlib.Structures.OrdersEx]
PositiveOrderedTypeBits.bits_lt [in Stdlib.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.compare [in Stdlib.Structures.OrdersEx]
PositiveOrderedTypeBits.compare [in Stdlib.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.eq [in Stdlib.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.eqb [in Stdlib.Structures.OrdersEx]
PositiveOrderedTypeBits.eqb_eq [in Stdlib.Structures.OrdersEx]
PositiveOrderedTypeBits.eq_trans [in Stdlib.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.eq_sym [in Stdlib.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.eq_refl [in Stdlib.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.lt [in Stdlib.Structures.OrdersEx]
PositiveOrderedTypeBits.lt [in Stdlib.Structures.OrderedTypeEx]
PositiveOrderedTypeBits.t [in Stdlib.Structures.OrdersEx]
PositiveOrderedTypeBits.t [in Stdlib.Structures.OrderedTypeEx]
PositiveSet.add [in Stdlib.MSets.MSetPositive]
PositiveSet.add [in Stdlib.FSets.FSetPositive]
PositiveSet.cardinal [in Stdlib.MSets.MSetPositive]
PositiveSet.cardinal [in Stdlib.FSets.FSetPositive]
PositiveSet.choose [in Stdlib.MSets.MSetPositive]
PositiveSet.choose [in Stdlib.FSets.FSetPositive]
PositiveSet.compare [in Stdlib.MSets.MSetPositive]
PositiveSet.compare_bool [in Stdlib.MSets.MSetPositive]
PositiveSet.compare_fun [in Stdlib.FSets.FSetPositive]
PositiveSet.compare_bool [in Stdlib.FSets.FSetPositive]
PositiveSet.diff [in Stdlib.MSets.MSetPositive]
PositiveSet.diff [in Stdlib.FSets.FSetPositive]
PositiveSet.elements [in Stdlib.MSets.MSetPositive]
PositiveSet.elements [in Stdlib.FSets.FSetPositive]
PositiveSet.elt [in Stdlib.MSets.MSetPositive]
PositiveSet.elt [in Stdlib.FSets.FSetPositive]
PositiveSet.Empty [in Stdlib.MSets.MSetPositive]
PositiveSet.empty [in Stdlib.MSets.MSetPositive]
PositiveSet.Empty [in Stdlib.FSets.FSetPositive]
PositiveSet.empty [in Stdlib.FSets.FSetPositive]
PositiveSet.eq [in Stdlib.MSets.MSetPositive]
PositiveSet.eq [in Stdlib.FSets.FSetPositive]
PositiveSet.Equal [in Stdlib.MSets.MSetPositive]
PositiveSet.equal [in Stdlib.MSets.MSetPositive]
PositiveSet.Equal [in Stdlib.FSets.FSetPositive]
PositiveSet.equal [in Stdlib.FSets.FSetPositive]
PositiveSet.Exists [in Stdlib.MSets.MSetPositive]
PositiveSet.Exists [in Stdlib.FSets.FSetPositive]
PositiveSet.exists_ [in Stdlib.MSets.MSetPositive]
PositiveSet.exists_ [in Stdlib.FSets.FSetPositive]
PositiveSet.filter [in Stdlib.MSets.MSetPositive]
PositiveSet.filter [in Stdlib.FSets.FSetPositive]
PositiveSet.fold [in Stdlib.MSets.MSetPositive]
PositiveSet.fold [in Stdlib.FSets.FSetPositive]
PositiveSet.For_all [in Stdlib.MSets.MSetPositive]
PositiveSet.for_all [in Stdlib.MSets.MSetPositive]
PositiveSet.For_all [in Stdlib.FSets.FSetPositive]
PositiveSet.for_all [in Stdlib.FSets.FSetPositive]
PositiveSet.In [in Stdlib.MSets.MSetPositive]
PositiveSet.In [in Stdlib.FSets.FSetPositive]
PositiveSet.inter [in Stdlib.MSets.MSetPositive]
PositiveSet.inter [in Stdlib.FSets.FSetPositive]
PositiveSet.is_empty [in Stdlib.MSets.MSetPositive]
PositiveSet.is_empty [in Stdlib.FSets.FSetPositive]
PositiveSet.lt [in Stdlib.MSets.MSetPositive]
PositiveSet.lt [in Stdlib.FSets.FSetPositive]
PositiveSet.max_elt [in Stdlib.MSets.MSetPositive]
PositiveSet.max_elt [in Stdlib.FSets.FSetPositive]
PositiveSet.mem [in Stdlib.MSets.MSetPositive]
PositiveSet.mem [in Stdlib.FSets.FSetPositive]
PositiveSet.min_elt [in Stdlib.MSets.MSetPositive]
PositiveSet.min_elt [in Stdlib.FSets.FSetPositive]
PositiveSet.node [in Stdlib.MSets.MSetPositive]
PositiveSet.node [in Stdlib.FSets.FSetPositive]
PositiveSet.omap [in Stdlib.FSets.FSetPositive]
PositiveSet.partition [in Stdlib.MSets.MSetPositive]
PositiveSet.partition [in Stdlib.FSets.FSetPositive]
PositiveSet.remove [in Stdlib.MSets.MSetPositive]
PositiveSet.remove [in Stdlib.FSets.FSetPositive]
PositiveSet.rev [in Stdlib.MSets.MSetPositive]
PositiveSet.rev [in Stdlib.FSets.FSetPositive]
PositiveSet.rev_append [in Stdlib.MSets.MSetPositive]
PositiveSet.rev_append [in Stdlib.FSets.FSetPositive]
PositiveSet.singleton [in Stdlib.MSets.MSetPositive]
PositiveSet.singleton [in Stdlib.FSets.FSetPositive]
PositiveSet.Subset [in Stdlib.MSets.MSetPositive]
PositiveSet.subset [in Stdlib.MSets.MSetPositive]
PositiveSet.Subset [in Stdlib.FSets.FSetPositive]
PositiveSet.subset [in Stdlib.FSets.FSetPositive]
PositiveSet.t [in Stdlib.MSets.MSetPositive]
PositiveSet.t [in Stdlib.FSets.FSetPositive]
PositiveSet.tree_ind [in Stdlib.MSets.MSetPositive]
PositiveSet.tree_ind [in Stdlib.FSets.FSetPositive]
PositiveSet.union [in Stdlib.MSets.MSetPositive]
PositiveSet.union [in Stdlib.FSets.FSetPositive]
PositiveSet.xelements [in Stdlib.MSets.MSetPositive]
PositiveSet.xelements [in Stdlib.FSets.FSetPositive]
PositiveSet.xexists [in Stdlib.MSets.MSetPositive]
PositiveSet.xexists [in Stdlib.FSets.FSetPositive]
PositiveSet.xfilter [in Stdlib.MSets.MSetPositive]
PositiveSet.xfilter [in Stdlib.FSets.FSetPositive]
PositiveSet.xfold [in Stdlib.MSets.MSetPositive]
PositiveSet.xfold [in Stdlib.FSets.FSetPositive]
PositiveSet.xforall [in Stdlib.MSets.MSetPositive]
PositiveSet.xforall [in Stdlib.FSets.FSetPositive]
PositiveSet.xpartition [in Stdlib.MSets.MSetPositive]
PositiveSet.xpartition [in Stdlib.FSets.FSetPositive]
positive_sind [in Stdlib.Numbers.BinNums]
positive_rec [in Stdlib.Numbers.BinNums]
positive_ind [in Stdlib.Numbers.BinNums]
positive_rect [in Stdlib.Numbers.BinNums]
positive_to_int [in Stdlib.Numbers.Cyclic.Int63.Cyclic63]
positive_to_int_rec [in Stdlib.Numbers.Cyclic.Int63.Cyclic63]
Positive_as_OT.eq_dec [in Stdlib.Structures.OrderedTypeEx]
Positive_as_OT.compare [in Stdlib.Structures.OrderedTypeEx]
Positive_as_OT.lt_trans [in Stdlib.Structures.OrderedTypeEx]
Positive_as_OT.lt [in Stdlib.Structures.OrderedTypeEx]
Positive_as_OT.eq_trans [in Stdlib.Structures.OrderedTypeEx]
Positive_as_OT.eq_sym [in Stdlib.Structures.OrderedTypeEx]
Positive_as_OT.eq_refl [in Stdlib.Structures.OrderedTypeEx]
Positive_as_OT.eq [in Stdlib.Structures.OrderedTypeEx]
Positive_as_OT.t [in Stdlib.Structures.OrderedTypeEx]
positivity_seq [in Stdlib.Reals.AltSeries]
posreal_half [in Stdlib.Reals.RIneq]
posreal_one [in Stdlib.Reals.RIneq]
pos_Rl [in Stdlib.Reals.RList]
pos_bin_app [in Stdlib.Strings.BinaryString]
pos_eq [in Stdlib.rtauto.Rtauto]
pos_hex_app [in Stdlib.Strings.HexString]
pos_to_z [in Stdlib.Numbers.AltBinNotations]
pos_of_z [in Stdlib.Numbers.AltBinNotations]
pos_oct_app [in Stdlib.Strings.OctalString]
Pos_is_pow2 [in Stdlib.Reals.Cauchy.QExtra]
Pos_log2ceil_plus1 [in Stdlib.Reals.Cauchy.QExtra]
Pos_log2floor_plus1 [in Stdlib.Reals.Cauchy.QExtra]
pos_of_int [in Stdlib.extraction.ExtrOcamlIntConv]
pos_mod [in Stdlib.Numbers.Cyclic.Int63.Cyclic63]
Pos.add [in Stdlib.PArith.BinPosDef]
Pos.add_carry [in Stdlib.PArith.BinPosDef]
Pos.compare [in Stdlib.PArith.BinPosDef]
Pos.compare_cont [in Stdlib.PArith.BinPosDef]
Pos.divide [in Stdlib.PArith.BinPosDef]
Pos.div2 [in Stdlib.PArith.BinPosDef]
Pos.div2_up [in Stdlib.PArith.BinPosDef]
Pos.double_pred_mask [in Stdlib.PArith.BinPosDef]
Pos.double_mask [in Stdlib.PArith.BinPosDef]
Pos.eq [in Stdlib.PArith.BinPos]
Pos.eqb [in Stdlib.PArith.BinPosDef]
Pos.eq_equiv [in Stdlib.PArith.BinPos]
Pos.gcd [in Stdlib.PArith.BinPosDef]
Pos.gcdn [in Stdlib.PArith.BinPosDef]
Pos.ge [in Stdlib.PArith.BinPos]
Pos.ggcd [in Stdlib.PArith.BinPosDef]
Pos.ggcdn [in Stdlib.PArith.BinPosDef]
Pos.gt [in Stdlib.PArith.BinPos]
Pos.iter [in Stdlib.PArith.BinPosDef]
Pos.iter_op [in Stdlib.PArith.BinPosDef]
Pos.land [in Stdlib.PArith.BinPosDef]
Pos.ldiff [in Stdlib.PArith.BinPosDef]
Pos.le [in Stdlib.PArith.BinPos]
Pos.leb [in Stdlib.PArith.BinPosDef]
Pos.le_lteq [in Stdlib.PArith.BinPos]
Pos.lor [in Stdlib.PArith.BinPosDef]
Pos.lt [in Stdlib.PArith.BinPos]
Pos.ltb [in Stdlib.PArith.BinPosDef]
Pos.lxor [in Stdlib.PArith.BinPosDef]
Pos.mask_sind [in Stdlib.PArith.BinPosDef]
Pos.mask_rec [in Stdlib.PArith.BinPosDef]
Pos.mask_ind [in Stdlib.PArith.BinPosDef]
Pos.mask_rect [in Stdlib.PArith.BinPosDef]
Pos.mask2cmp [in Stdlib.PArith.BinPos]
Pos.max [in Stdlib.PArith.BinPosDef]
Pos.min [in Stdlib.PArith.BinPosDef]
Pos.mul [in Stdlib.PArith.BinPosDef]
Pos.Ndouble [in Stdlib.PArith.BinPosDef]
Pos.Nsucc_double [in Stdlib.PArith.BinPosDef]
Pos.of_num_int [in Stdlib.PArith.BinPosDef]
Pos.of_hex_int [in Stdlib.PArith.BinPosDef]
Pos.of_int [in Stdlib.PArith.BinPosDef]
Pos.of_num_uint [in Stdlib.PArith.BinPosDef]
Pos.of_hex_uint [in Stdlib.PArith.BinPosDef]
Pos.of_hex_uint_acc [in Stdlib.PArith.BinPosDef]
Pos.of_uint [in Stdlib.PArith.BinPosDef]
Pos.of_uint_acc [in Stdlib.PArith.BinPosDef]
Pos.of_succ_nat [in Stdlib.PArith.BinPosDef]
Pos.of_nat [in Stdlib.PArith.BinPosDef]
Pos.peanoView [in Stdlib.PArith.BinPos]
Pos.PeanoView_iter [in Stdlib.PArith.BinPos]
Pos.peanoView_xI [in Stdlib.PArith.BinPos]
Pos.peanoView_xO [in Stdlib.PArith.BinPos]
Pos.PeanoView_sind [in Stdlib.PArith.BinPos]
Pos.PeanoView_rec [in Stdlib.PArith.BinPos]
Pos.PeanoView_ind [in Stdlib.PArith.BinPos]
Pos.PeanoView_rect [in Stdlib.PArith.BinPos]
Pos.peano_ind [in Stdlib.PArith.BinPos]
Pos.peano_rec [in Stdlib.PArith.BinPos]
Pos.peano_rect [in Stdlib.PArith.BinPos]
Pos.pow [in Stdlib.PArith.BinPosDef]
Pos.pred [in Stdlib.PArith.BinPosDef]
Pos.pred_mask [in Stdlib.PArith.BinPosDef]
Pos.pred_N [in Stdlib.PArith.BinPosDef]
Pos.pred_double [in Stdlib.PArith.BinPosDef]
Pos.shiftl [in Stdlib.PArith.BinPosDef]
Pos.shiftl_nat [in Stdlib.PArith.BinPosDef]
Pos.shiftr [in Stdlib.PArith.BinPosDef]
Pos.shiftr_nat [in Stdlib.PArith.BinPosDef]
Pos.size [in Stdlib.PArith.BinPosDef]
Pos.size_nat [in Stdlib.PArith.BinPosDef]
Pos.sqrt [in Stdlib.PArith.BinPosDef]
Pos.sqrtrem [in Stdlib.PArith.BinPosDef]
Pos.sqrtrem_step [in Stdlib.PArith.BinPosDef]
Pos.SqrtSpec_sind [in Stdlib.PArith.BinPos]
Pos.SqrtSpec_ind [in Stdlib.PArith.BinPos]
Pos.square [in Stdlib.PArith.BinPosDef]
Pos.sub [in Stdlib.PArith.BinPosDef]
Pos.SubMaskSpec_sind [in Stdlib.PArith.BinPos]
Pos.SubMaskSpec_ind [in Stdlib.PArith.BinPos]
Pos.sub_mask_carry [in Stdlib.PArith.BinPosDef]
Pos.sub_mask [in Stdlib.PArith.BinPosDef]
Pos.succ [in Stdlib.PArith.BinPosDef]
Pos.succ_double_mask [in Stdlib.PArith.BinPosDef]
Pos.switch_Eq [in Stdlib.PArith.BinPos]
Pos.t [in Stdlib.PArith.BinPosDef]
Pos.testbit [in Stdlib.PArith.BinPosDef]
Pos.testbit_nat [in Stdlib.PArith.BinPosDef]
Pos.to_num_hex_int [in Stdlib.PArith.BinPosDef]
Pos.to_num_int [in Stdlib.PArith.BinPosDef]
Pos.to_hex_int [in Stdlib.PArith.BinPosDef]
Pos.to_int [in Stdlib.PArith.BinPosDef]
Pos.to_num_hex_uint [in Stdlib.PArith.BinPosDef]
Pos.to_num_uint [in Stdlib.PArith.BinPosDef]
Pos.to_hex_uint [in Stdlib.PArith.BinPosDef]
Pos.to_little_hex_uint [in Stdlib.PArith.BinPosDef]
Pos.to_uint [in Stdlib.PArith.BinPosDef]
Pos.to_little_uint [in Stdlib.PArith.BinPosDef]
Pos.to_nat [in Stdlib.PArith.BinPosDef]
pow [in Stdlib.Logic.Berardi]
Pow [in Stdlib.Relations.Relation_Operators]
pow [in Stdlib.Init.Nat]
pow [in Stdlib.Reals.Rpow_def]
pow [in Stdlib.setoid_ring.Integral_domain]
pow [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
powerRZ [in Stdlib.Reals.Rfunctions]
Power_set_PO [in Stdlib.Sets.Powerset]
Power_set_sind [in Stdlib.Sets.Powerset]
Power_set_ind [in Stdlib.Sets.Powerset]
pow_N_gen [in Stdlib.setoid_ring.Ncring_polynom]
pow_pos_gen [in Stdlib.setoid_ring.Ncring_polynom]
pow_fct [in Stdlib.Reals.Ranalysis1]
pow_2_n [in Stdlib.Reals.Rsqrt_def]
pow_N [in Stdlib.setoid_ring.Ncring]
pow_pos [in Stdlib.setoid_ring.Ncring]
pow_N_th [in Stdlib.setoid_ring.Ring_theory]
pow_N [in Stdlib.setoid_ring.Ring_theory]
pow_pos [in Stdlib.setoid_ring.Ring_theory]
Pphi [in Stdlib.setoid_ring.Ncring_polynom]
Pphi [in Stdlib.micromega.EnvRing]
Pphi [in Stdlib.setoid_ring.Ring_polynom]
Pphi_dev [in Stdlib.setoid_ring.Ring_polynom]
Pphi_pow [in Stdlib.setoid_ring.Ring_polynom]
Pphi_avoid [in Stdlib.setoid_ring.Ring_polynom]
Ppow_N [in Stdlib.setoid_ring.Ncring_polynom]
Ppow_pos [in Stdlib.setoid_ring.Ncring_polynom]
Ppow_N [in Stdlib.micromega.EnvRing]
Ppow_pos [in Stdlib.micromega.EnvRing]
Ppow_N [in Stdlib.setoid_ring.Ring_polynom]
Ppow_pos [in Stdlib.setoid_ring.Ring_polynom]
prec [in Stdlib.Floats.FloatOps]
pred [in Stdlib.ssr.ssrbool]
pred [in Stdlib.Init.Nat]
pred [in Stdlib.Numbers.Cyclic.Int63.Uint63]
predArgType [in Stdlib.ssr.ssrbool]
predC [in Stdlib.ssr.ssrbool]
predc [in Stdlib.Numbers.Cyclic.Int63.Uint63]
predD [in Stdlib.ssr.ssrbool]
predI [in Stdlib.ssr.ssrbool]
PredicateExtensionality [in Stdlib.Logic.Diaconescu]
predicate_union [in Stdlib.Classes.RelationClasses]
predicate_intersection [in Stdlib.Classes.RelationClasses]
predicate_implication [in Stdlib.Classes.RelationClasses]
predicate_equivalence [in Stdlib.Classes.RelationClasses]
predicate_exists [in Stdlib.Classes.RelationClasses]
predicate_all [in Stdlib.Classes.RelationClasses]
PredOfSimpl.coerce [in Stdlib.ssr.ssrbool]
predPredType [in Stdlib.ssr.ssrbool]
predT [in Stdlib.ssr.ssrbool]
predU [in Stdlib.ssr.ssrbool]
pred_oapp [in Stdlib.ssr.ssrbool]
pred_of_mem [in Stdlib.ssr.ssrbool]
pred_of_argType [in Stdlib.ssr.ssrbool]
pred_of_minus [in Stdlib.Arith.PeanoNat]
pred0 [in Stdlib.ssr.ssrbool]
prefix [in Stdlib.Strings.String]
preim [in Stdlib.ssr.ssrbool]
Preorder_sind [in Stdlib.Sets.Relations_1]
Preorder_rec [in Stdlib.Sets.Relations_1]
Preorder_ind [in Stdlib.Sets.Relations_1]
Preorder_rect [in Stdlib.Sets.Relations_1]
pre_symmetric [in Stdlib.ssr.ssrbool]
pre_atan [in Stdlib.Reals.Ratan]
prime_dec [in Stdlib.ZArith.Znumtheory]
prime_dec_aux [in Stdlib.ZArith.Znumtheory]
prime_sind [in Stdlib.ZArith.Znumtheory]
prime_rec [in Stdlib.ZArith.Znumtheory]
prime_ind [in Stdlib.ZArith.Znumtheory]
prime_rect [in Stdlib.ZArith.Znumtheory]
prime' [in Stdlib.ZArith.Znumtheory]
primitive [in Stdlib.Reals.RiemannInt]
Prim2SF [in Stdlib.Floats.FloatOps]
printer [in Stdlib.Numbers.Cyclic.Int63.Sint63]
printer [in Stdlib.Floats.PrimFloat]
printer [in Stdlib.Numbers.Cyclic.Int63.PrimInt63]
prod_sind [in Stdlib.Init.Datatypes]
prod_rec [in Stdlib.Init.Datatypes]
prod_ind [in Stdlib.Init.Datatypes]
prod_rect [in Stdlib.Init.Datatypes]
prod_pos_nat [in Stdlib.micromega.ZMicromega]
prod_f_R0 [in Stdlib.Reals.Rprod]
prod_of_sigT [in Stdlib.Init.Specif]
prog_linear_search [in Stdlib.Logic.ConstructiveEpsilon]
projT1 [in Stdlib.Init.Specif]
projT1_of_sigT2_eq [in Stdlib.Init.Specif]
projT1_eq [in Stdlib.Init.Specif]
projT2 [in Stdlib.Init.Specif]
projT2_of_sigT2_eq [in Stdlib.Init.Specif]
projT2_eq [in Stdlib.Init.Specif]
projT3 [in Stdlib.Init.Specif]
projT3_eq [in Stdlib.Init.Specif]
proj1_inf [in Stdlib.Logic.ChoiceFacts]
proj1_sig_of_sig2_eq [in Stdlib.Init.Specif]
proj1_sig_eq [in Stdlib.Init.Specif]
proj1_sig [in Stdlib.Init.Specif]
proj2_sig_of_sig2_eq [in Stdlib.Init.Specif]
proj2_sig_eq [in Stdlib.Init.Specif]
proj2_sig [in Stdlib.Init.Specif]
proj3_sig_eq [in Stdlib.Init.Specif]
proj3_sig [in Stdlib.Init.Specif]
ProofIrrelevance [in Stdlib.Logic.ChoiceFacts]
ProofIrrelevanceTheory.eq_indd [in Stdlib.Logic.ProofIrrelevanceFacts]
proof_sind [in Stdlib.rtauto.Rtauto]
proof_rec [in Stdlib.rtauto.Rtauto]
proof_ind [in Stdlib.rtauto.Rtauto]
proof_rect [in Stdlib.rtauto.Rtauto]
proof_irrelevance [in Stdlib.Logic.ClassicalFacts]
proof_sind [in Stdlib.micromega.Ztac]
proof_rec [in Stdlib.micromega.Ztac]
proof_ind [in Stdlib.micromega.Ztac]
proof_rect [in Stdlib.micromega.Ztac]
proper_flip_proper [in Stdlib.Classes.Morphisms]
proper_flip_proper [in Stdlib.Classes.CMorphisms]
PropOp_iff [in Stdlib.micromega.ZifyClasses]
Props.bst_ind [in Stdlib.MSets.MSetGenTree]
Props.cardinal_spec [in Stdlib.MSets.MSetGenTree]
Props.Cmp [in Stdlib.MSets.MSetGenTree]
Props.Empty [in Stdlib.MSets.MSetGenTree]
Props.eq [in Stdlib.MSets.MSetGenTree]
Props.Equal [in Stdlib.MSets.MSetGenTree]
Props.Exists [in Stdlib.MSets.MSetGenTree]
Props.flatten_e [in Stdlib.MSets.MSetGenTree]
Props.For_all [in Stdlib.MSets.MSetGenTree]
Props.gtb_tree [in Stdlib.MSets.MSetGenTree]
Props.gt_tree [in Stdlib.MSets.MSetGenTree]
Props.In [in Stdlib.MSets.MSetGenTree]
Props.isok [in Stdlib.MSets.MSetGenTree]
Props.IsOk [in Stdlib.MSets.MSetGenTree]
Props.lt [in Stdlib.MSets.MSetGenTree]
Props.ltb_tree [in Stdlib.MSets.MSetGenTree]
Props.lt_tree [in Stdlib.MSets.MSetGenTree]
Props.Subset [in Stdlib.MSets.MSetGenTree]
Props.tree_ind [in Stdlib.MSets.MSetGenTree]
PropUOp_iff [in Stdlib.micromega.ZifyClasses]
prop_on2 [in Stdlib.ssr.ssrbool]
prop_on1 [in Stdlib.ssr.ssrbool]
prop_in3 [in Stdlib.ssr.ssrbool]
prop_in21 [in Stdlib.ssr.ssrbool]
prop_in12 [in Stdlib.ssr.ssrbool]
prop_in111 [in Stdlib.ssr.ssrbool]
prop_in2 [in Stdlib.ssr.ssrbool]
prop_in11 [in Stdlib.ssr.ssrbool]
prop_in1 [in Stdlib.ssr.ssrbool]
prop_for [in Stdlib.ssr.ssrbool]
prop_extensionality [in Stdlib.Logic.ClassicalFacts]
prop_degeneracy [in Stdlib.Logic.ClassicalFacts]
protected_to_nat [in Stdlib.setoid_ring.ArithRing]
protect_term [in Stdlib.ssr.ssreflect]
provable_prop_extensionality [in Stdlib.Logic.ClassicalFacts]
Psatz_sind [in Stdlib.micromega.RingMicromega]
Psatz_rec [in Stdlib.micromega.RingMicromega]
Psatz_ind [in Stdlib.micromega.RingMicromega]
Psatz_rect [in Stdlib.micromega.RingMicromega]
Pser [in Stdlib.Reals.Rseries]
Psquare [in Stdlib.setoid_ring.Ncring_polynom]
Psquare [in Stdlib.micromega.EnvRing]
PStringNotations.id_string [in Stdlib.Strings.PrimString]
Psub [in Stdlib.setoid_ring.Ncring_polynom]
psub [in Stdlib.micromega.ZMicromega]
psub [in Stdlib.micromega.RingMicromega]
Psub [in Stdlib.micromega.EnvRing]
Psub [in Stdlib.setoid_ring.Ring_polynom]
psubC [in Stdlib.micromega.RingMicromega]
PsubC [in Stdlib.micromega.EnvRing]
PsubC [in Stdlib.setoid_ring.Ring_polynom]
PsubC_ok [in Stdlib.micromega.RingMicromega]
PsubI [in Stdlib.micromega.EnvRing]
PsubI [in Stdlib.setoid_ring.Ring_polynom]
PSubstL [in Stdlib.micromega.EnvRing]
PSubstL [in Stdlib.setoid_ring.Ring_polynom]
PSubstL1 [in Stdlib.micromega.EnvRing]
PSubstL1 [in Stdlib.setoid_ring.Ring_polynom]
PsubX [in Stdlib.micromega.EnvRing]
PsubX [in Stdlib.setoid_ring.Ring_polynom]
ps_atan [in Stdlib.Reals.Ratan]
ps_atan_exists_1 [in Stdlib.Reals.Ratan]
ps_atan_exists_01 [in Stdlib.Reals.Ratan]
push [in Stdlib.rtauto.Bintree]
P_nth_sind [in Stdlib.Arith.Between]
P_nth_ind [in Stdlib.Arith.Between]
P_Rmin_stt [in Stdlib.Reals.Rpower]
P' [in Stdlib.Logic.ConstructiveEpsilon]
P0 [in Stdlib.setoid_ring.Ncring_polynom]
P0 [in Stdlib.micromega.EnvRing]
P0 [in Stdlib.setoid_ring.Ring_polynom]
P0Z [in Stdlib.nsatz.NsatzTactic]
P1 [in Stdlib.setoid_ring.Ncring_polynom]
P1 [in Stdlib.micromega.EnvRing]
P1 [in Stdlib.setoid_ring.Ring_polynom]
| 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 | (26071 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 | (1003 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 | (815 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 | (1771 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 | (589 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 | (961 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 | (12021 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 | (508 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 | (308 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 | (479 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 | (496 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 | (906 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 | (1204 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 | (4844 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 | (166 entries) |