| 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) |
N (definition)
nan [in Stdlib.Floats.PrimFloat]napply_discard [in Stdlib.Numbers.NaryFunctions]
napply_then_last [in Stdlib.Numbers.NaryFunctions]
napply_except_last [in Stdlib.Numbers.NaryFunctions]
napply_cst [in Stdlib.Numbers.NaryFunctions]
nary_congruence_statement [in Stdlib.ssr.ssreflect]
NatOrder.leb [in Stdlib.Sorting.Mergesort]
NatOrder.t [in Stdlib.Sorting.Mergesort]
nat_of_ascii [in Stdlib.Strings.Ascii]
nat_sind [in Stdlib.Init.Datatypes]
nat_rec [in Stdlib.Init.Datatypes]
nat_ind [in Stdlib.Init.Datatypes]
nat_rect [in Stdlib.Init.Datatypes]
nat_po [in Stdlib.Sets.Integers]
nat_noteq_bool [in Stdlib.Arith.Bool_nat]
nat_eq_bool [in Stdlib.Arith.Bool_nat]
nat_gt_le_bool [in Stdlib.Arith.Bool_nat]
nat_le_gt_bool [in Stdlib.Arith.Bool_nat]
nat_ge_lt_bool [in Stdlib.Arith.Bool_nat]
nat_lt_ge_bool [in Stdlib.Arith.Bool_nat]
nat_of_int [in Stdlib.extraction.ExtrOcamlIntConv]
nat_compare_alt [in Stdlib.Arith.Compare_dec]
Nat_as_OT.eq_dec [in Stdlib.Structures.OrderedTypeEx]
Nat_as_OT.compare [in Stdlib.Structures.OrderedTypeEx]
Nat_as_OT.lt [in Stdlib.Structures.OrderedTypeEx]
Nat_as_OT.eq_trans [in Stdlib.Structures.OrderedTypeEx]
Nat_as_OT.eq_sym [in Stdlib.Structures.OrderedTypeEx]
Nat_as_OT.eq_refl [in Stdlib.Structures.OrderedTypeEx]
Nat_as_OT.eq [in Stdlib.Structures.OrderedTypeEx]
Nat_as_OT.t [in Stdlib.Structures.OrderedTypeEx]
Nat.divide [in Stdlib.Arith.PeanoNat]
Nat.double_add [in Stdlib.Arith.PeanoNat]
Nat.double_S [in Stdlib.Arith.PeanoNat]
Nat.eq [in Stdlib.Arith.PeanoNat]
Nat.eq_equiv [in Stdlib.Arith.PeanoNat]
Nat.Even [in Stdlib.Arith.PeanoNat]
Nat.EvenT [in Stdlib.Arith.PeanoNat]
Nat.Even_alt_Odd_alt_sind [in Stdlib.Arith.PeanoNat]
Nat.Even_alt_Odd_alt_ind [in Stdlib.Arith.PeanoNat]
Nat.Even_alt_sind [in Stdlib.Arith.PeanoNat]
Nat.Even_alt_ind [in Stdlib.Arith.PeanoNat]
Nat.Even_Odd_dec [in Stdlib.Arith.PeanoNat]
Nat.le [in Stdlib.Arith.PeanoNat]
Nat.lt [in Stdlib.Arith.PeanoNat]
Nat.Odd [in Stdlib.Arith.PeanoNat]
Nat.OddT [in Stdlib.Arith.PeanoNat]
Nat.Odd_alt_Even_alt_sind [in Stdlib.Arith.PeanoNat]
Nat.Odd_alt_Even_alt_ind [in Stdlib.Arith.PeanoNat]
Nat.Odd_alt_sind [in Stdlib.Arith.PeanoNat]
Nat.Odd_alt_ind [in Stdlib.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.shiftl_spec_high [in Stdlib.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.shiftr_spec [in Stdlib.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.testbit_even_succ [in Stdlib.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.testbit_odd_succ [in Stdlib.Arith.PeanoNat]
Nat.recursion [in Stdlib.Arith.PeanoNat]
Nat.sqrt_spec [in Stdlib.Arith.PeanoNat]
NBitsProp.b2n [in Stdlib.Numbers.Natural.Abstract.NBits]
NBitsProp.clearbit [in Stdlib.Numbers.Natural.Abstract.NBits]
NBitsProp.eqf [in Stdlib.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot [in Stdlib.Numbers.Natural.Abstract.NBits]
NBitsProp.ones [in Stdlib.Numbers.Natural.Abstract.NBits]
NBitsProp.setbit [in Stdlib.Numbers.Natural.Abstract.NBits]
Nbound [in Stdlib.Reals.RiemannInt_SF]
nb_digits [in Stdlib.Init.Decimal]
nb_digits [in Stdlib.Init.Hexadecimal]
ncurry [in Stdlib.Numbers.NaryFunctions]
NdefOpsProp.def_mul [in Stdlib.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.def_add [in Stdlib.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.even [in Stdlib.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half [in Stdlib.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_aux [in Stdlib.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.if_zero [in Stdlib.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.log [in Stdlib.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.ltb [in Stdlib.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.pow [in Stdlib.Numbers.Natural.Abstract.NDefOps]
NDivProp0.div_add_l [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_add [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_le_compat_l [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_le_lower_bound [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_lt [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_str_pos_iff [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_small_iff [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_str_pos [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_mul [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_1_l [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_1_r [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_small [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_same [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_unique_exact [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_unique [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_mod_unique [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mod_small_iff [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mod_1_l [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mod_1_r [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mod_small [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mod_unique [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mod_upper_bound [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mul_succ_div_gt [in Stdlib.Numbers.Natural.Abstract.NDiv0]
negate [in Stdlib.micromega.ZMicromega]
negate [in Stdlib.micromega.RingMicromega]
negb [in Stdlib.Init.Datatypes]
neg_zero [in Stdlib.Floats.PrimFloat]
neg_infinity [in Stdlib.Floats.PrimFloat]
neighbourhood [in Stdlib.Reals.Rtopology]
neq [in Stdlib.ZArith.Znat]
nequiv_decb [in Stdlib.Classes.SetoidDec]
nequiv_dec [in Stdlib.Classes.SetoidDec]
nequiv_decb [in Stdlib.Classes.EquivDec]
nequiv_dec [in Stdlib.Classes.EquivDec]
neq_0_lt_stt [in Stdlib.Arith.Arith_base]
nesym [in Stdlib.ssr.ssrfun]
NewtonInt [in Stdlib.Reals.NewtonInt]
Newton_integrable [in Stdlib.Reals.NewtonInt]
new_location [in Stdlib.Floats.SpecFloat]
new_location_odd [in Stdlib.Floats.SpecFloat]
new_location_even [in Stdlib.Floats.SpecFloat]
nfold [in Stdlib.Numbers.NaryFunctions]
nfold_list [in Stdlib.Numbers.NaryFunctions]
nfold_bis [in Stdlib.Numbers.NaryFunctions]
NFormula [in Stdlib.micromega.RingMicromega]
nformula_of_cutting_plane [in Stdlib.micromega.ZMicromega]
nformula_plus_nformula [in Stdlib.micromega.RingMicromega]
nformula_times_nformula [in Stdlib.micromega.RingMicromega]
nfun [in Stdlib.Numbers.NaryFunctions]
nfun_to_nfun_bis [in Stdlib.Numbers.NaryFunctions]
nfun_to_nfun [in Stdlib.Numbers.NaryFunctions]
NGcdProp.Bezout [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_gcd_iff [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_pos_le [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_factor_r [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_factor_l [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_mul_r [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_mul_l [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_add_r [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_antisym [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_trans [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_refl [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_0_l [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_0_r [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_1_l [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_1_r [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_mul_diag_l [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_eq_0 [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_eq_0_r [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_eq_0_l [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_assoc [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_comm [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_unique_alt [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_unique [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_diag [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_0_r [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_0_l [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.mul_divide_cancel_r [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.mul_divide_cancel_l [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.mul_divide_mono_r [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.mul_divide_mono_l [in Stdlib.Numbers.Natural.Abstract.NGcd]
nhyps_of_psatz [in Stdlib.micromega.RingMicromega]
NilEmpty.int_of_string [in Stdlib.Numbers.HexadecimalString]
NilEmpty.int_of_string [in Stdlib.Numbers.DecimalString]
NilEmpty.string_of_int [in Stdlib.Numbers.HexadecimalString]
NilEmpty.string_of_uint [in Stdlib.Numbers.HexadecimalString]
NilEmpty.string_of_int [in Stdlib.Numbers.DecimalString]
NilEmpty.string_of_uint [in Stdlib.Numbers.DecimalString]
NilEmpty.uint_of_string [in Stdlib.Numbers.HexadecimalString]
NilEmpty.uint_of_string [in Stdlib.Numbers.DecimalString]
NilZero.int_of_string [in Stdlib.Numbers.HexadecimalString]
NilZero.int_of_string [in Stdlib.Numbers.DecimalString]
NilZero.string_of_int [in Stdlib.Numbers.HexadecimalString]
NilZero.string_of_uint [in Stdlib.Numbers.HexadecimalString]
NilZero.string_of_int [in Stdlib.Numbers.DecimalString]
NilZero.string_of_uint [in Stdlib.Numbers.DecimalString]
NilZero.uint_of_string [in Stdlib.Numbers.HexadecimalString]
NilZero.uint_of_string [in Stdlib.Numbers.DecimalString]
NLcmProp.lcm [in Stdlib.Numbers.Natural.Abstract.NLcm]
NLcmProp0.divide_lcm_iff [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.divide_lcm_eq_r [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.divide_lcm_r [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.divide_lcm_l [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.gcd_1_lcm_mul [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.gcd_div_swap [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.gcd_div_gcd [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.lcm [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.lcm_mul_mono_r [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.lcm_mul_mono_l [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.lcm_eq_0 [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.lcm_diag [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.lcm_1_r [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.lcm_1_l [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.lcm_0_r [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.lcm_0_l [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.lcm_assoc [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.lcm_divide_iff [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.lcm_comm [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.lcm_least [in Stdlib.Numbers.Natural.Abstract.NLcm0]
Nleb [in Stdlib.NArith.Ndec]
NMulOrderProp.mul_eq_1 [in Stdlib.Numbers.Natural.Abstract.NMulOrder]
node [in Stdlib.micromega.ZMicromega]
NodepOfDep.Add [in Stdlib.FSets.FSetBridge]
NodepOfDep.add [in Stdlib.FSets.FSetBridge]
NodepOfDep.cardinal [in Stdlib.FSets.FSetBridge]
NodepOfDep.choose [in Stdlib.FSets.FSetBridge]
NodepOfDep.compare [in Stdlib.FSets.FSetBridge]
NodepOfDep.diff [in Stdlib.FSets.FSetBridge]
NodepOfDep.elements [in Stdlib.FSets.FSetBridge]
NodepOfDep.elt [in Stdlib.FSets.FSetBridge]
NodepOfDep.Empty [in Stdlib.FSets.FSetBridge]
NodepOfDep.empty [in Stdlib.FSets.FSetBridge]
NodepOfDep.eq [in Stdlib.FSets.FSetBridge]
NodepOfDep.Equal [in Stdlib.FSets.FSetBridge]
NodepOfDep.equal [in Stdlib.FSets.FSetBridge]
NodepOfDep.eq_trans [in Stdlib.FSets.FSetBridge]
NodepOfDep.eq_sym [in Stdlib.FSets.FSetBridge]
NodepOfDep.eq_refl [in Stdlib.FSets.FSetBridge]
NodepOfDep.eq_dec [in Stdlib.FSets.FSetBridge]
NodepOfDep.Exists [in Stdlib.FSets.FSetBridge]
NodepOfDep.exists_ [in Stdlib.FSets.FSetBridge]
NodepOfDep.filter [in Stdlib.FSets.FSetBridge]
NodepOfDep.fold [in Stdlib.FSets.FSetBridge]
NodepOfDep.For_all [in Stdlib.FSets.FSetBridge]
NodepOfDep.for_all [in Stdlib.FSets.FSetBridge]
NodepOfDep.f_dec [in Stdlib.FSets.FSetBridge]
NodepOfDep.In [in Stdlib.FSets.FSetBridge]
NodepOfDep.inter [in Stdlib.FSets.FSetBridge]
NodepOfDep.In_1 [in Stdlib.FSets.FSetBridge]
NodepOfDep.is_empty [in Stdlib.FSets.FSetBridge]
NodepOfDep.lt [in Stdlib.FSets.FSetBridge]
NodepOfDep.lt_not_eq [in Stdlib.FSets.FSetBridge]
NodepOfDep.lt_trans [in Stdlib.FSets.FSetBridge]
NodepOfDep.max_elt [in Stdlib.FSets.FSetBridge]
NodepOfDep.mem [in Stdlib.FSets.FSetBridge]
NodepOfDep.min_elt [in Stdlib.FSets.FSetBridge]
NodepOfDep.partition [in Stdlib.FSets.FSetBridge]
NodepOfDep.remove [in Stdlib.FSets.FSetBridge]
NodepOfDep.singleton [in Stdlib.FSets.FSetBridge]
NodepOfDep.Subset [in Stdlib.FSets.FSetBridge]
NodepOfDep.subset [in Stdlib.FSets.FSetBridge]
NodepOfDep.t [in Stdlib.FSets.FSetBridge]
NodepOfDep.union [in Stdlib.FSets.FSetBridge]
nodup [in Stdlib.Lists.List]
NoDupA_sind [in Stdlib.Lists.SetoidList]
NoDupA_ind [in Stdlib.Lists.SetoidList]
NoDup_sind [in Stdlib.Lists.List]
NoDup_ind [in Stdlib.Lists.List]
Noetherian [in Stdlib.Sets.Relations_3]
noetherian_sind [in Stdlib.Sets.Relations_3]
noetherian_rec [in Stdlib.Sets.Relations_3]
noetherian_ind [in Stdlib.Sets.Relations_3]
noetherian_rect [in Stdlib.Sets.Relations_3]
NonPropType.call [in Stdlib.ssr.ssreflect]
NonPropType.check [in Stdlib.ssr.ssreflect]
NonPropType.maybeProp [in Stdlib.ssr.ssreflect]
NonPropType.test_negative [in Stdlib.ssr.ssreflect]
NonPropType.test_Prop [in Stdlib.ssr.ssreflect]
Nopp [in Stdlib.setoid_ring.InitialRing]
NoRetractFromSmallPropositionToProp.El [in Stdlib.Logic.Hurkens]
NoRetractFromSmallPropositionToProp.NProp [in Stdlib.Logic.Hurkens]
NoRetractFromTypeToProp.Type1 [in Stdlib.Logic.Hurkens]
NoRetractFromTypeToProp.Type2 [in Stdlib.Logic.Hurkens]
NoRetractToModalProposition.El [in Stdlib.Logic.Hurkens]
NoRetractToModalProposition.Forall [in Stdlib.Logic.Hurkens]
NoRetractToModalProposition.MProp [in Stdlib.Logic.Hurkens]
NoRetractToNegativeProp.El [in Stdlib.Logic.Hurkens]
NoRetractToNegativeProp.NProp [in Stdlib.Logic.Hurkens]
norm [in Stdlib.Init.Decimal]
norm [in Stdlib.micromega.RingMicromega]
norm [in Stdlib.Init.Hexadecimal]
norm [in Stdlib.nsatz.NsatzTactic]
normalise [in Stdlib.micromega.ZMicromega]
normalise [in Stdlib.micromega.RingMicromega]
normQ [in Stdlib.micromega.QMicromega]
normZ [in Stdlib.micromega.ZMicromega]
norm_subst [in Stdlib.setoid_ring.Ncring_polynom]
norm_aux [in Stdlib.setoid_ring.Ncring_polynom]
norm_subst [in Stdlib.micromega.EnvRing]
norm_aux [in Stdlib.micromega.EnvRing]
norm_subst [in Stdlib.setoid_ring.Ring_polynom]
norm_aux [in Stdlib.setoid_ring.Ring_polynom]
not [in Stdlib.Init.Logic]
NotConstant [in Stdlib.setoid_ring.Ncring_initial]
NotConstant [in Stdlib.setoid_ring.InitialRing]
notF [in Stdlib.ssr.ssrbool]
notT [in Stdlib.Init.Logic]
notzerop [in Stdlib.Arith.Bool_nat]
notzerop_bool [in Stdlib.Arith.Bool_nat]
Not_b [in Stdlib.Logic.Berardi]
not_eq_false_beq [in Stdlib.Bool.BoolEq]
no_cond [in Stdlib.Reals.Ranalysis1]
NPEadd [in Stdlib.setoid_ring.Field_theory]
NPEequiv [in Stdlib.setoid_ring.Field_theory]
NPEmul [in Stdlib.setoid_ring.Field_theory]
NPEopp [in Stdlib.setoid_ring.Field_theory]
NPEpow [in Stdlib.setoid_ring.Field_theory]
NPEsub [in Stdlib.setoid_ring.Field_theory]
NPowProp.pow_lt_mono [in Stdlib.Numbers.Natural.Abstract.NPow]
NPowProp.pow_2_r [in Stdlib.Numbers.Natural.Abstract.NPow]
NPowProp.pow_1_r [in Stdlib.Numbers.Natural.Abstract.NPow]
nprod [in Stdlib.Numbers.NaryFunctions]
nprod_of_list [in Stdlib.Numbers.NaryFunctions]
nprod_to_list [in Stdlib.Numbers.NaryFunctions]
NSqrtProp.sqrt_add_le [in Stdlib.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_mul_below [in Stdlib.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_lt_lin [in Stdlib.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_2 [in Stdlib.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_1 [in Stdlib.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_0 [in Stdlib.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_lt_cancel [in Stdlib.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_le_mono [in Stdlib.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_unique [in Stdlib.Numbers.Natural.Abstract.NSqrt]
NStrongRecProp.strong_rec0 [in Stdlib.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec [in Stdlib.Numbers.Natural.Abstract.NStrongRec]
Nsub [in Stdlib.setoid_ring.InitialRing]
NSubProp.le_alt [in Stdlib.Numbers.Natural.Abstract.NSub]
NSubProp.lt_alt [in Stdlib.Numbers.Natural.Abstract.NSub]
nth [in Stdlib.micromega.Env]
nth [in Stdlib.Vectors.VectorDef]
nth [in Stdlib.Lists.List]
nth [in Stdlib.setoid_ring.BinList]
nth_order [in Stdlib.Vectors.VectorDef]
nth_default [in Stdlib.Lists.List]
nth_error [in Stdlib.Lists.List]
nth_ok [in Stdlib.Lists.List]
NtoZ [in Stdlib.setoid_ring.Field_theory]
null_sind [in Stdlib.btauto.Algebra]
null_rec [in Stdlib.btauto.Algebra]
null_ind [in Stdlib.btauto.Algebra]
null_rect [in Stdlib.btauto.Algebra]
number_eq_dec [in Stdlib.Init.Number]
nuncurry [in Stdlib.Numbers.NaryFunctions]
Nwadd [in Stdlib.setoid_ring.InitialRing]
Nwcons [in Stdlib.setoid_ring.InitialRing]
Nweq_bool [in Stdlib.setoid_ring.InitialRing]
NwI [in Stdlib.setoid_ring.InitialRing]
Nwmul [in Stdlib.setoid_ring.InitialRing]
NwO [in Stdlib.setoid_ring.InitialRing]
Nwopp [in Stdlib.setoid_ring.InitialRing]
Nword [in Stdlib.setoid_ring.InitialRing]
Nwscal [in Stdlib.setoid_ring.InitialRing]
Nwsub [in Stdlib.setoid_ring.InitialRing]
Nw_is0 [in Stdlib.setoid_ring.InitialRing]
NZCyclicAxiomsMod.add [in Stdlib.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.eq [in Stdlib.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.mul [in Stdlib.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.one [in Stdlib.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.pred [in Stdlib.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.sub [in Stdlib.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.succ [in Stdlib.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.t [in Stdlib.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.two [in Stdlib.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.zero [in Stdlib.Numbers.Cyclic.Abstract.NZCyclic]
NZDomainProp.initial [in Stdlib.Numbers.NatInt.NZDomain]
NZGcdSpec.divide [in Stdlib.Numbers.NatInt.NZGcd]
nzhead [in Stdlib.Init.Decimal]
nzhead [in Stdlib.Init.Hexadecimal]
NZLog2UpProp.log2_up [in Stdlib.Numbers.NatInt.NZLog]
NZOfNat.ofnat [in Stdlib.Numbers.NatInt.NZDomain]
NZOrderProp.le_lteq [in Stdlib.Numbers.NatInt.NZOrder]
NZOrderProp.lt_total [in Stdlib.Numbers.NatInt.NZOrder]
NZOrderProp.lt_compat [in Stdlib.Numbers.NatInt.NZOrder]
NZOrderProp.Private_OrderTac.IsTotal.le_lteq [in Stdlib.Numbers.NatInt.NZOrder]
NZOrderProp.Private_OrderTac.IsTotal.lt_total [in Stdlib.Numbers.NatInt.NZOrder]
NZOrderProp.Private_OrderTac.IsTotal.lt_compat [in Stdlib.Numbers.NatInt.NZOrder]
NZOrderProp.Private_OrderTac.IsTotal.lt_strorder [in Stdlib.Numbers.NatInt.NZOrder]
NZOrderProp.Private_OrderTac.IsTotal.eq_equiv [in Stdlib.Numbers.NatInt.NZOrder]
NZParity.Even [in Stdlib.Numbers.NatInt.NZParity]
NZParity.Odd [in Stdlib.Numbers.NatInt.NZParity]
NZSqrtUpProp.sqrt_up [in Stdlib.Numbers.NatInt.NZSqrt]
nztail [in Stdlib.Init.Decimal]
nztail [in Stdlib.Numbers.HexadecimalFacts]
nztail [in Stdlib.Init.Hexadecimal]
nztail [in Stdlib.Numbers.DecimalFacts]
nztail_int [in Stdlib.Init.Decimal]
nztail_int [in Stdlib.Init.Hexadecimal]
N_of_ascii [in Stdlib.Strings.Ascii]
N_of_digits [in Stdlib.Strings.Ascii]
N_sind [in Stdlib.Numbers.BinNums]
N_rec [in Stdlib.Numbers.BinNums]
N_ind [in Stdlib.Numbers.BinNums]
N_rect [in Stdlib.Numbers.BinNums]
n_to_z [in Stdlib.Numbers.AltBinNotations]
n_of_z [in Stdlib.Numbers.AltBinNotations]
N_rec_double [in Stdlib.NArith.BinNat]
N_ind_double [in Stdlib.NArith.BinNat]
n_of_int [in Stdlib.extraction.ExtrOcamlIntConv]
N_as_OT.eq_dec [in Stdlib.Structures.OrderedTypeEx]
N_as_OT.compare [in Stdlib.Structures.OrderedTypeEx]
N_as_OT.lt_not_eq [in Stdlib.Structures.OrderedTypeEx]
N_as_OT.lt_trans [in Stdlib.Structures.OrderedTypeEx]
N_as_OT.lt [in Stdlib.Structures.OrderedTypeEx]
N_as_OT.eq_trans [in Stdlib.Structures.OrderedTypeEx]
N_as_OT.eq_sym [in Stdlib.Structures.OrderedTypeEx]
N_as_OT.eq_refl [in Stdlib.Structures.OrderedTypeEx]
N_as_OT.eq [in Stdlib.Structures.OrderedTypeEx]
N_as_OT.t [in Stdlib.Structures.OrderedTypeEx]
N.add [in Stdlib.NArith.BinNatDef]
N.add_wd [in Stdlib.NArith.BinNat]
N.binary_ind [in Stdlib.NArith.BinNat]
N.binary_rec [in Stdlib.NArith.BinNat]
N.binary_rect [in Stdlib.NArith.BinNat]
N.compare [in Stdlib.NArith.BinNatDef]
N.discr [in Stdlib.NArith.BinNat]
N.div [in Stdlib.NArith.BinNatDef]
N.divide [in Stdlib.NArith.BinNat]
N.div_eucl [in Stdlib.NArith.BinNatDef]
N.div_wd [in Stdlib.NArith.BinNat]
N.div2 [in Stdlib.NArith.BinNatDef]
N.double [in Stdlib.NArith.BinNatDef]
N.eq [in Stdlib.NArith.BinNat]
N.eqb [in Stdlib.NArith.BinNatDef]
N.eq_dec [in Stdlib.NArith.BinNat]
N.eq_equiv [in Stdlib.NArith.BinNat]
N.even [in Stdlib.NArith.BinNatDef]
N.Even [in Stdlib.NArith.BinNat]
N.gcd [in Stdlib.NArith.BinNatDef]
N.ge [in Stdlib.NArith.BinNat]
N.ggcd [in Stdlib.NArith.BinNatDef]
N.gt [in Stdlib.NArith.BinNat]
N.iter [in Stdlib.NArith.BinNatDef]
N.land [in Stdlib.NArith.BinNatDef]
N.ldiff [in Stdlib.NArith.BinNatDef]
N.le [in Stdlib.NArith.BinNat]
N.leb [in Stdlib.NArith.BinNatDef]
N.log2 [in Stdlib.NArith.BinNatDef]
N.lor [in Stdlib.NArith.BinNatDef]
N.lt [in Stdlib.NArith.BinNat]
N.ltb [in Stdlib.NArith.BinNatDef]
N.lt_wd [in Stdlib.NArith.BinNat]
N.lxor [in Stdlib.NArith.BinNatDef]
N.max [in Stdlib.NArith.BinNatDef]
N.min [in Stdlib.NArith.BinNatDef]
N.modulo [in Stdlib.NArith.BinNatDef]
N.mod_wd [in Stdlib.NArith.BinNat]
N.mul [in Stdlib.NArith.BinNatDef]
N.mul_wd [in Stdlib.NArith.BinNat]
N.odd [in Stdlib.NArith.BinNatDef]
N.Odd [in Stdlib.NArith.BinNat]
N.of_num_int [in Stdlib.NArith.BinNatDef]
N.of_hex_int [in Stdlib.NArith.BinNatDef]
N.of_int [in Stdlib.NArith.BinNatDef]
N.of_num_uint [in Stdlib.NArith.BinNatDef]
N.of_hex_uint [in Stdlib.NArith.BinNatDef]
N.of_uint [in Stdlib.NArith.BinNatDef]
N.of_nat [in Stdlib.NArith.BinNatDef]
N.one [in Stdlib.NArith.BinNatDef]
N.peano_rec [in Stdlib.NArith.BinNat]
N.peano_ind [in Stdlib.NArith.BinNat]
N.peano_rect [in Stdlib.NArith.BinNat]
N.pos_div_eucl [in Stdlib.NArith.BinNatDef]
N.pow [in Stdlib.NArith.BinNatDef]
N.pow_wd [in Stdlib.NArith.BinNat]
N.pred [in Stdlib.NArith.BinNatDef]
N.pred_wd [in Stdlib.NArith.BinNat]
N.recursion [in Stdlib.NArith.BinNat]
N.shiftl [in Stdlib.NArith.BinNatDef]
N.shiftl_nat [in Stdlib.NArith.BinNatDef]
N.shiftr [in Stdlib.NArith.BinNatDef]
N.shiftr_nat [in Stdlib.NArith.BinNatDef]
N.size [in Stdlib.NArith.BinNatDef]
N.size_nat [in Stdlib.NArith.BinNatDef]
N.sqrt [in Stdlib.NArith.BinNatDef]
N.sqrtrem [in Stdlib.NArith.BinNatDef]
N.square [in Stdlib.NArith.BinNatDef]
N.sub [in Stdlib.NArith.BinNatDef]
N.sub_wd [in Stdlib.NArith.BinNat]
N.succ [in Stdlib.NArith.BinNatDef]
N.succ_pos [in Stdlib.NArith.BinNatDef]
N.succ_double [in Stdlib.NArith.BinNatDef]
N.succ_wd [in Stdlib.NArith.BinNat]
N.t [in Stdlib.NArith.BinNatDef]
N.testbit [in Stdlib.NArith.BinNatDef]
N.testbit_nat [in Stdlib.NArith.BinNatDef]
N.testbit_wd [in Stdlib.NArith.BinNat]
N.to_num_hex_int [in Stdlib.NArith.BinNatDef]
N.to_num_int [in Stdlib.NArith.BinNatDef]
N.to_hex_int [in Stdlib.NArith.BinNatDef]
N.to_int [in Stdlib.NArith.BinNatDef]
N.to_num_hex_uint [in Stdlib.NArith.BinNatDef]
N.to_num_uint [in Stdlib.NArith.BinNatDef]
N.to_hex_uint [in Stdlib.NArith.BinNatDef]
N.to_uint [in Stdlib.NArith.BinNatDef]
N.to_nat [in Stdlib.NArith.BinNatDef]
N.two [in Stdlib.NArith.BinNatDef]
N.zero [in Stdlib.NArith.BinNatDef]
| 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) |