| 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 | (22221 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 | (923 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 | (744 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 | (1480 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 | (501 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 | (10364 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 | (910 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 | (573 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 | (386 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 | (286 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 | (465 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 | (632 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 | (1133 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 | (3679 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 | (145 entries) |
N
N [module, in Coq.NArith.BinNatDef]N [module, in Coq.Numbers.Natural.Binary.NBinary]
N [section, in Coq.Strings.Byte]
N [module, in Coq.NArith.BinNat]
N [constructor, in Coq.micromega.Tauto]
N [inductive, in Coq.Numbers.BinNums]
NAdd [library]
NAddOrder [library]
NAddOrderProp [module, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderProp.add_pos_r [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderProp.add_pos_l [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderProp.le_add_r [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderProp.lt_lt_add_l [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderProp.lt_lt_add_r [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddProp [module, in Coq.Numbers.Natural.Abstract.NAdd]
NAddProp.add_pred_r [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddProp.add_pred_l [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddProp.eq_add_1 [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddProp.eq_add_succ [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddProp.eq_add_0 [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddProp.succ_add_discr [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
nandP [lemma, in Coq.ssr.ssrbool]
Nand_BVand [lemma, in Coq.NArith.Ndigits]
Nand_semantics [lemma, in Coq.NArith.Ndigits]
napply_discard [definition, in Coq.Numbers.NaryFunctions]
napply_then_last [definition, in Coq.Numbers.NaryFunctions]
napply_except_last [definition, in Coq.Numbers.NaryFunctions]
napply_cst [definition, in Coq.Numbers.NaryFunctions]
NArith [library]
NArithRing [library]
narrow_interval_lower_bound [lemma, in Coq.micromega.ZMicromega]
NaryFunctions [library]
nary_congruence [lemma, in Coq.ssr.ssreflect]
nary_congruence_statement [definition, in Coq.ssr.ssreflect]
Nat [module, in Coq.Numbers.Natural.Peano.NPeano]
nat [section, in Coq.Strings.Byte]
nat [inductive, in Coq.Init.Datatypes]
Nat [module, in Coq.Arith.PeanoNat]
Nat [library]
Nath [lemma, in Coq.setoid_ring.InitialRing]
natinf [inductive, in Coq.NArith.Ndist]
natlike_rec3 [lemma, in Coq.ZArith.Wf_Z]
natlike_rec2 [lemma, in Coq.ZArith.Wf_Z]
natlike_rec [lemma, in Coq.ZArith.Wf_Z]
natlike_ind [lemma, in Coq.ZArith.Wf_Z]
NatOrder [module, in Coq.Sorting.Mergesort]
NatOrder.leb [definition, in Coq.Sorting.Mergesort]
NatOrder.leb_total [lemma, in Coq.Sorting.Mergesort]
NatOrder.t [definition, in Coq.Sorting.Mergesort]
_ <=? _ [notation, in Coq.Sorting.Mergesort]
NatSeq [section, in Coq.Lists.List]
NatSort [module, in Coq.Sorting.Mergesort]
natSRth [lemma, in Coq.setoid_ring.ArithRing]
nat_rect_wd [instance, in Coq.Numbers.NatInt.NZDomain]
nat_of_N_of_nat [abbreviation, in Coq.NArith.Nnat]
nat_of_Nmin [abbreviation, in Coq.NArith.Nnat]
nat_of_Nmax [abbreviation, in Coq.NArith.Nnat]
nat_of_Ncompare [abbreviation, in Coq.NArith.Nnat]
nat_of_Ndiv2 [abbreviation, in Coq.NArith.Nnat]
nat_of_Npred [abbreviation, in Coq.NArith.Nnat]
nat_of_Nminus [abbreviation, in Coq.NArith.Nnat]
nat_of_Nmult [abbreviation, in Coq.NArith.Nnat]
nat_of_Nplus [abbreviation, in Coq.NArith.Nnat]
nat_of_Nsucc [abbreviation, in Coq.NArith.Nnat]
nat_of_Ndouble_plus_one [abbreviation, in Coq.NArith.Nnat]
nat_of_Ndouble [abbreviation, in Coq.NArith.Nnat]
nat_of_N_inj [abbreviation, in Coq.NArith.Nnat]
Nat_as_DT [module, in Coq.Structures.DecidableTypeEx]
nat_po [definition, in Coq.Sets.Integers]
nat_N_Z [lemma, in Coq.ZArith.Znat]
nat_morph_N [lemma, in Coq.setoid_ring.ArithRing]
nat_ascii_bounded [lemma, in Coq.Strings.Ascii]
nat_ascii_embedding [lemma, in Coq.Strings.Ascii]
nat_of_ascii [definition, in Coq.Strings.Ascii]
Nat_as_DT [module, in Coq.Structures.OrdersEx]
Nat_as_OT [module, in Coq.Structures.OrdersEx]
nat_eq_eqdec [instance, in Coq.Classes.SetoidDec]
nat_of_int [definition, in Coq.extraction.ExtrOcamlIntConv]
nat_rect_plus [lemma, in Coq.Init.Peano]
nat_rect_succ_r [lemma, in Coq.Init.Peano]
nat_double_ind [lemma, in Coq.Init.Peano]
nat_case [lemma, in Coq.Init.Peano]
nat_of_P [abbreviation, in Coq.PArith.BinPos]
nat_of_N [abbreviation, in Coq.NArith.BinNat]
nat_bijection_Permutation [lemma, in Coq.Sorting.Permutation]
nat_noteq_bool [definition, in Coq.Arith.Bool_nat]
nat_eq_bool [definition, in Coq.Arith.Bool_nat]
nat_gt_le_bool [definition, in Coq.Arith.Bool_nat]
nat_le_gt_bool [definition, in Coq.Arith.Bool_nat]
nat_ge_lt_bool [definition, in Coq.Arith.Bool_nat]
nat_lt_ge_bool [definition, in Coq.Arith.Bool_nat]
nat_total_order [lemma, in Coq.Arith.Lt]
Nat_as_OT.eq_dec [definition, in Coq.Structures.OrderedTypeEx]
Nat_as_OT.compare [definition, in Coq.Structures.OrderedTypeEx]
Nat_as_OT.lt_not_eq [lemma, in Coq.Structures.OrderedTypeEx]
Nat_as_OT.lt_trans [lemma, in Coq.Structures.OrderedTypeEx]
Nat_as_OT.lt [definition, in Coq.Structures.OrderedTypeEx]
Nat_as_OT.eq_trans [definition, in Coq.Structures.OrderedTypeEx]
Nat_as_OT.eq_sym [definition, in Coq.Structures.OrderedTypeEx]
Nat_as_OT.eq_refl [definition, in Coq.Structures.OrderedTypeEx]
Nat_as_OT.eq [definition, in Coq.Structures.OrderedTypeEx]
Nat_as_OT.t [definition, in Coq.Structures.OrderedTypeEx]
Nat_as_OT [module, in Coq.Structures.OrderedTypeEx]
nat_of_P_gt_Gt_compare_complement_morphism [definition, in Coq.PArith.Pnat]
nat_of_P_lt_Lt_compare_complement_morphism [lemma, in Coq.PArith.Pnat]
nat_of_P_gt_Gt_compare_morphism [lemma, in Coq.PArith.Pnat]
nat_of_P_lt_Lt_compare_morphism [lemma, in Coq.PArith.Pnat]
nat_of_P_minus_morphism [lemma, in Coq.PArith.Pnat]
nat_of_P_o_P_of_succ_nat_eq_succ [abbreviation, in Coq.PArith.Pnat]
nat_of_P_compare_morphism [abbreviation, in Coq.PArith.Pnat]
nat_of_P_mult_morphism [abbreviation, in Coq.PArith.Pnat]
nat_of_P_plus_morphism [abbreviation, in Coq.PArith.Pnat]
nat_of_P_succ_morphism [abbreviation, in Coq.PArith.Pnat]
nat_of_P_of_succ_nat [abbreviation, in Coq.PArith.Pnat]
nat_of_P_inj [abbreviation, in Coq.PArith.Pnat]
nat_of_P_inj_iff [abbreviation, in Coq.PArith.Pnat]
nat_of_P_pos [abbreviation, in Coq.PArith.Pnat]
nat_of_P_is_S [abbreviation, in Coq.PArith.Pnat]
nat_of_P_xI [abbreviation, in Coq.PArith.Pnat]
nat_of_P_xO [abbreviation, in Coq.PArith.Pnat]
nat_of_P_xH [abbreviation, in Coq.PArith.Pnat]
nat_of_bigint [definition, in Coq.extraction.ExtrOcamlBigIntConv]
nat_eq_eqdec [instance, in Coq.Classes.EquivDec]
nat_compare_equiv [lemma, in Coq.Arith.Compare_dec]
nat_compare_alt [definition, in Coq.Arith.Compare_dec]
nat_compare_Gt_gt [lemma, in Coq.Arith.Compare_dec]
nat_compare_Lt_lt [lemma, in Coq.Arith.Compare_dec]
nat_compare_eq [lemma, in Coq.Arith.Compare_dec]
nat_compare_ge [lemma, in Coq.Arith.Compare_dec]
nat_compare_le [lemma, in Coq.Arith.Compare_dec]
nat_compare_gt [lemma, in Coq.Arith.Compare_dec]
nat_compare_lt [lemma, in Coq.Arith.Compare_dec]
nat_compare_S [abbreviation, in Coq.Arith.Compare_dec]
Nat.add_succ_l [lemma, in Coq.Arith.PeanoNat]
Nat.add_0_l [lemma, in Coq.Arith.PeanoNat]
Nat.add_wd [instance, in Coq.Arith.PeanoNat]
Nat.bi_induction [lemma, in Coq.Arith.PeanoNat]
Nat.compare_succ [lemma, in Coq.Arith.PeanoNat]
Nat.compare_antisym [lemma, in Coq.Arith.PeanoNat]
Nat.compare_le_iff [lemma, in Coq.Arith.PeanoNat]
Nat.compare_lt_iff [lemma, in Coq.Arith.PeanoNat]
Nat.compare_eq_iff [lemma, in Coq.Arith.PeanoNat]
Nat.divide [definition, in Coq.Arith.PeanoNat]
Nat.divmod_spec [lemma, in Coq.Arith.PeanoNat]
Nat.div_mod [lemma, in Coq.Arith.PeanoNat]
Nat.div_wd [instance, in Coq.Arith.PeanoNat]
Nat.div2_spec [lemma, in Coq.Arith.PeanoNat]
Nat.div2_bitwise [lemma, in Coq.Arith.PeanoNat]
Nat.div2_decr [lemma, in Coq.Arith.PeanoNat]
Nat.div2_succ_double [lemma, in Coq.Arith.PeanoNat]
Nat.div2_double [lemma, in Coq.Arith.PeanoNat]
Nat.double_twice [lemma, in Coq.Arith.PeanoNat]
Nat.eq [definition, in Coq.Arith.PeanoNat]
Nat.eqb_eq [lemma, in Coq.Arith.PeanoNat]
Nat.eq_dec [lemma, in Coq.Arith.PeanoNat]
Nat.eq_equiv [definition, in Coq.Arith.PeanoNat]
Nat.Even [definition, in Coq.Arith.PeanoNat]
Nat.even_spec [lemma, in Coq.Arith.PeanoNat]
Nat.gcd_nonneg [lemma, in Coq.Arith.PeanoNat]
Nat.gcd_greatest [lemma, in Coq.Arith.PeanoNat]
Nat.gcd_divide_r [lemma, in Coq.Arith.PeanoNat]
Nat.gcd_divide_l [lemma, in Coq.Arith.PeanoNat]
Nat.gcd_divide [lemma, in Coq.Arith.PeanoNat]
Nat.land_spec [lemma, in Coq.Arith.PeanoNat]
Nat.ldiff_spec [lemma, in Coq.Arith.PeanoNat]
Nat.le [definition, in Coq.Arith.PeanoNat]
Nat.leb_le [lemma, in Coq.Arith.PeanoNat]
Nat.le_div2 [lemma, in Coq.Arith.PeanoNat]
Nat.log2_nonpos [lemma, in Coq.Arith.PeanoNat]
Nat.log2_spec [lemma, in Coq.Arith.PeanoNat]
Nat.log2_iter_spec [lemma, in Coq.Arith.PeanoNat]
Nat.lor_spec [lemma, in Coq.Arith.PeanoNat]
Nat.lt [definition, in Coq.Arith.PeanoNat]
Nat.ltb_lt [lemma, in Coq.Arith.PeanoNat]
Nat.lt_div2 [lemma, in Coq.Arith.PeanoNat]
Nat.lt_succ_r [lemma, in Coq.Arith.PeanoNat]
Nat.lt_wd [instance, in Coq.Arith.PeanoNat]
Nat.lxor_spec [lemma, in Coq.Arith.PeanoNat]
Nat.max_r [lemma, in Coq.Arith.PeanoNat]
Nat.max_l [lemma, in Coq.Arith.PeanoNat]
Nat.min_r [lemma, in Coq.Arith.PeanoNat]
Nat.min_l [lemma, in Coq.Arith.PeanoNat]
Nat.mod_bound_pos [lemma, in Coq.Arith.PeanoNat]
Nat.mod_wd [instance, in Coq.Arith.PeanoNat]
Nat.mul_succ_l [lemma, in Coq.Arith.PeanoNat]
Nat.mul_0_l [lemma, in Coq.Arith.PeanoNat]
Nat.mul_wd [instance, in Coq.Arith.PeanoNat]
Nat.Odd [definition, in Coq.Arith.PeanoNat]
Nat.odd_bitwise [lemma, in Coq.Arith.PeanoNat]
Nat.odd_spec [lemma, in Coq.Arith.PeanoNat]
Nat.one_succ [lemma, in Coq.Arith.PeanoNat]
Nat.pow_succ_r [lemma, in Coq.Arith.PeanoNat]
Nat.pow_0_r [lemma, in Coq.Arith.PeanoNat]
Nat.pow_neg_r [lemma, in Coq.Arith.PeanoNat]
Nat.pow_wd [instance, in Coq.Arith.PeanoNat]
Nat.pred_0 [lemma, in Coq.Arith.PeanoNat]
Nat.pred_succ [lemma, in Coq.Arith.PeanoNat]
Nat.pred_wd [instance, in Coq.Arith.PeanoNat]
Nat.Private_Parity.Odd_2 [lemma, in Coq.Arith.PeanoNat]
Nat.Private_Parity.Odd_0 [lemma, in Coq.Arith.PeanoNat]
Nat.Private_Parity.Even_2 [lemma, in Coq.Arith.PeanoNat]
Nat.Private_Parity.Even_1 [lemma, in Coq.Arith.PeanoNat]
Nat.Private_Parity [module, in Coq.Arith.PeanoNat]
Nat.recursion [definition, in Coq.Arith.PeanoNat]
Nat.recursion_succ [lemma, in Coq.Arith.PeanoNat]
Nat.recursion_0 [lemma, in Coq.Arith.PeanoNat]
Nat.recursion_wd [instance, in Coq.Arith.PeanoNat]
Nat.shiftl_spec_high [definition, in Coq.Arith.PeanoNat]
Nat.shiftl_spec_low [lemma, in Coq.Arith.PeanoNat]
Nat.shiftl_specif_high [lemma, in Coq.Arith.PeanoNat]
Nat.shiftr_spec [definition, in Coq.Arith.PeanoNat]
Nat.shiftr_specif [lemma, in Coq.Arith.PeanoNat]
Nat.sqrt_neg [lemma, in Coq.Arith.PeanoNat]
Nat.sqrt_spec [definition, in Coq.Arith.PeanoNat]
Nat.sqrt_specif [lemma, in Coq.Arith.PeanoNat]
Nat.sqrt_iter_spec [lemma, in Coq.Arith.PeanoNat]
Nat.square_spec [lemma, in Coq.Arith.PeanoNat]
Nat.sub_succ_r [lemma, in Coq.Arith.PeanoNat]
Nat.sub_0_r [lemma, in Coq.Arith.PeanoNat]
Nat.sub_wd [instance, in Coq.Arith.PeanoNat]
Nat.succ_wd [instance, in Coq.Arith.PeanoNat]
Nat.tail_mul_spec [lemma, in Coq.Arith.PeanoNat]
Nat.tail_addmul_spec [lemma, in Coq.Arith.PeanoNat]
Nat.tail_add_spec [lemma, in Coq.Arith.PeanoNat]
Nat.testbit_neg_r [lemma, in Coq.Arith.PeanoNat]
Nat.testbit_even_succ [definition, in Coq.Arith.PeanoNat]
Nat.testbit_odd_succ [definition, in Coq.Arith.PeanoNat]
Nat.testbit_bitwise_2 [lemma, in Coq.Arith.PeanoNat]
Nat.testbit_bitwise_1 [lemma, in Coq.Arith.PeanoNat]
Nat.testbit_even_succ' [lemma, in Coq.Arith.PeanoNat]
Nat.testbit_odd_succ' [lemma, in Coq.Arith.PeanoNat]
Nat.testbit_even_0 [lemma, in Coq.Arith.PeanoNat]
Nat.testbit_odd_0 [lemma, in Coq.Arith.PeanoNat]
Nat.testbit_0_l [lemma, in Coq.Arith.PeanoNat]
Nat.testbit_wd [instance, in Coq.Arith.PeanoNat]
Nat.two_succ [lemma, in Coq.Arith.PeanoNat]
( _ | _ ) (nat_scope) [notation, in Coq.Arith.PeanoNat]
Nat2N [module, in Coq.NArith.Nnat]
Nat2N.id [lemma, in Coq.NArith.Nnat]
Nat2N.inj [lemma, in Coq.NArith.Nnat]
Nat2N.inj_iter [lemma, in Coq.NArith.Nnat]
Nat2N.inj_max [lemma, in Coq.NArith.Nnat]
Nat2N.inj_min [lemma, in Coq.NArith.Nnat]
Nat2N.inj_compare [lemma, in Coq.NArith.Nnat]
Nat2N.inj_div2 [lemma, in Coq.NArith.Nnat]
Nat2N.inj_mul [lemma, in Coq.NArith.Nnat]
Nat2N.inj_sub [lemma, in Coq.NArith.Nnat]
Nat2N.inj_add [lemma, in Coq.NArith.Nnat]
Nat2N.inj_pred [lemma, in Coq.NArith.Nnat]
Nat2N.inj_succ [lemma, in Coq.NArith.Nnat]
Nat2N.inj_succ_double [lemma, in Coq.NArith.Nnat]
Nat2N.inj_double [lemma, in Coq.NArith.Nnat]
Nat2N.inj_iff [lemma, in Coq.NArith.Nnat]
Nat2Pos [module, in Coq.PArith.Pnat]
Nat2Pos.id [lemma, in Coq.PArith.Pnat]
Nat2Pos.id_max [lemma, in Coq.PArith.Pnat]
Nat2Pos.inj [lemma, in Coq.PArith.Pnat]
Nat2Pos.inj_max [lemma, in Coq.PArith.Pnat]
Nat2Pos.inj_min [lemma, in Coq.PArith.Pnat]
Nat2Pos.inj_sub [lemma, in Coq.PArith.Pnat]
Nat2Pos.inj_compare [lemma, in Coq.PArith.Pnat]
Nat2Pos.inj_mul [lemma, in Coq.PArith.Pnat]
Nat2Pos.inj_add [lemma, in Coq.PArith.Pnat]
Nat2Pos.inj_pred [lemma, in Coq.PArith.Pnat]
Nat2Pos.inj_succ [lemma, in Coq.PArith.Pnat]
Nat2Pos.inj_iff [lemma, in Coq.PArith.Pnat]
Nat2Z [module, in Coq.ZArith.Znat]
Nat2Z.id [lemma, in Coq.ZArith.Znat]
Nat2Z.inj [lemma, in Coq.ZArith.Znat]
Nat2Z.inj_max [lemma, in Coq.ZArith.Znat]
Nat2Z.inj_min [lemma, in Coq.ZArith.Znat]
Nat2Z.inj_pred [lemma, in Coq.ZArith.Znat]
Nat2Z.inj_pred_max [lemma, in Coq.ZArith.Znat]
Nat2Z.inj_sub [lemma, in Coq.ZArith.Znat]
Nat2Z.inj_sub_max [lemma, in Coq.ZArith.Znat]
Nat2Z.inj_mul [lemma, in Coq.ZArith.Znat]
Nat2Z.inj_add [lemma, in Coq.ZArith.Znat]
Nat2Z.inj_abs_nat [lemma, in Coq.ZArith.Znat]
Nat2Z.inj_gt [lemma, in Coq.ZArith.Znat]
Nat2Z.inj_ge [lemma, in Coq.ZArith.Znat]
Nat2Z.inj_lt [lemma, in Coq.ZArith.Znat]
Nat2Z.inj_le [lemma, in Coq.ZArith.Znat]
Nat2Z.inj_compare [lemma, in Coq.ZArith.Znat]
Nat2Z.inj_iff [lemma, in Coq.ZArith.Znat]
Nat2Z.inj_succ [lemma, in Coq.ZArith.Znat]
Nat2Z.inj_0 [lemma, in Coq.ZArith.Znat]
Nat2Z.is_nonneg [lemma, in Coq.ZArith.Znat]
NAxiom [module, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxioms [library]
NAxiomsFullSig [module, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsFullSig' [module, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsMiniSig [module, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsMiniSig' [module, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsRec [module, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsRecSig [module, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsRecSig' [module, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsRec.recursion [axiom, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsRec.recursion_succ [axiom, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsRec.recursion_0 [axiom, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsRec.recursion_wd [instance, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig [module, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig' [module, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiom.pred_0 [axiom, in Coq.Numbers.Natural.Abstract.NAxioms]
NBase [library]
NBaseProp [module, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.case_analysis [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.DoubleInduction [section, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.DoubleInduction.R [variable, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.DoubleInduction.R_wd [variable, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.double_induction [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.eq_pred_0 [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.induction [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.le_0_l [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.neq_0_r [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.neq_0 [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.neq_0_succ [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.neq_succ_0 [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.PairInduction [section, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.PairInduction.A [variable, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.PairInduction.A_wd [variable, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.pair_induction [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.pred_inj [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.succ_pred [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.TwoDimensionalInduction [section, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.TwoDimensionalInduction.R [variable, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.TwoDimensionalInduction.R_wd [variable, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.two_dim_induction [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.zero_or_succ [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasicProp [module, in Coq.Numbers.Natural.Abstract.NProperties]
NBinary [library]
Nbit [abbreviation, in Coq.NArith.Ndigits]
NBits [library]
NBitsProp [module, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_nocarry_mod_lt_pow2 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_nocarry_lt_pow2 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_lnot_diag_low [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_nocarry_lxor [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_bit1 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_carry_bits [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_carry_div2 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_bit0 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_b2n_double_bit0 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_b2n_double_div2 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add3_bits_div2 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add3_bit0 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.are_bits [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.bits_inj_iff [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.bits_inj [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.bits_inj_0 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.bits_above_log2 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.bits_0 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.bit_log2 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.bit0_mod [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.bit0_eqb [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.bit0_odd [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.b2n [definition, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.b2n_bit0 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.b2n_div2 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.b2n_inj [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.b2n_proper [instance, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.clearbit [definition, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.clearbit_neq [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.clearbit_eq [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.clearbit_iff [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.clearbit_eqb [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.clearbit_wd [instance, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.clearbit_spec' [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.div_pow2_bits [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.div2_odd [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.div2_wd [instance, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.div2_div [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.div2_bits [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.double_bits_succ [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.eqf [definition, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.eqf_equiv [instance, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.exists_div2 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_lnot_diag_low [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_lnot_diag [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_ones_low [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_ones [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_ldiff [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_lor_distr_r [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_lor_distr_l [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_diag [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_assoc [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_comm [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_0_r [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_0_l [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_wd [instance, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_le [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_land_low [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_ones_l_low [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_ones_r_low [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_ones_r [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_ldiff_l [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_diag [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_0_r [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_0_l [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_wd [instance, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnextcarry [abbreviation, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot [definition, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_sub_low [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_lxor_r [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_lxor_l [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_ldiff_low [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_land_low [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_lor_low [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_ones [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_0_l [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_involutive [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_spec_high [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_spec_low [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_wd [instance, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.log2_lxor [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.log2_land [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.log2_lor [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.log2_shiftl [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.log2_shiftr [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.log2_bits_unique [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_lnot_diag_low [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_lnot_diag [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_ones_low [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_ldiff_and [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_land_distr_r [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_land_distr_l [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_eq_0_iff [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_eq_0_l [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_diag [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_assoc [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_comm [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_0_r [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_0_l [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_wd [instance, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_lor [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_lnot_lnot [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_assoc [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_comm [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_0_r [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_0_l [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_eq_0_iff [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_nilpotent [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_eq [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_wd [instance, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor3 [abbreviation, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.mod_pow2_bits_low [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.mod_pow2_bits_high [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.mul_pow2_bits_low [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.mul_pow2_bits_high [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.mul_pow2_bits_add [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.nextcarry [abbreviation, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.nocarry_equiv [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ones [definition, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ones_spec_iff [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ones_spec_high [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ones_spec_low [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ones_mod_pow2 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ones_div_pow2 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ones_add [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ones_equiv [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ones_wd [instance, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.pow_div_l [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.pow_sub_r [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.pow2_bits_eqb [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.pow2_bits_false [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.pow2_bits_true [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.setbit [definition, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.setbit_neq [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.setbit_eq [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.setbit_iff [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.setbit_eqb [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.setbit_wd [instance, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.setbit_spec' [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_ldiff [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_lor [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_land [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_lxor [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_eq_0_iff [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_0_l [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_0_r [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_1_l [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_shiftl [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_wd [instance, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_spec_alt [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_mul_pow2 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_spec_high' [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_ldiff [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_lor [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_land [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_lxor [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_eq_0 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_eq_0_iff [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_0_l [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_0_r [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_shiftl_r [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_shiftl_l [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_shiftr [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_wd [instance, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_div_pow2 [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_spec' [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.sub_nocarry_ldiff [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_eqf [instance, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_odd [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_unique [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_eqb [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_false [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_true [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_spec [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_spec' [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_succ_r [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_0_r [lemma, in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.xor3 [abbreviation, in Coq.Numbers.Natural.Abstract.NBits]
_ === _ [notation, in Coq.Numbers.Natural.Abstract.NBits]
Nbit_Bth [lemma, in Coq.NArith.Ndigits]
Nbit_Nsize [lemma, in Coq.NArith.Ndigits]
Nbit_faithful_iff [lemma, in Coq.NArith.Ndigits]
Nbit_faithful [lemma, in Coq.NArith.Ndigits]
Nbit_Ntestbit [lemma, in Coq.NArith.Ndigits]
Nbit0 [abbreviation, in Coq.NArith.Ndigits]
Nbit0_Blow [lemma, in Coq.NArith.Ndigits]
Nbit0_gt [lemma, in Coq.NArith.Ndigits]
Nbit0_less [lemma, in Coq.NArith.Ndigits]
Nbit0_correct [lemma, in Coq.NArith.Ndigits]
Nbit0_neq [lemma, in Coq.NArith.Ndec]
Nbound [definition, in Coq.Reals.RiemannInt_SF]
nb_digits [definition, in Coq.Init.Decimal]
Ncompare_antisym [lemma, in Coq.NArith.BinNat]
Ncompare_0 [abbreviation, in Coq.NArith.BinNat]
Ncompare_eq_correct [abbreviation, in Coq.NArith.BinNat]
Ncompare_Eq_eq [abbreviation, in Coq.NArith.BinNat]
Ncompare_Lt_Nltb [lemma, in Coq.NArith.Ndec]
Ncompare_Gt_Nltb [lemma, in Coq.NArith.Ndec]
Ncompare_Neqb [lemma, in Coq.NArith.Ndec]
Ncring [library]
Ncring_polynom [library]
Ncring_tac [library]
Ncring_initial [library]
ncurry [definition, in Coq.Numbers.NaryFunctions]
Ndec [library]
NDefOps [library]
NdefOpsProp [module, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.def_mul_mul [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.def_mul_succ_r [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.def_mul_0_r [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.def_mul_wd [instance, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.def_mul [definition, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.def_add_add [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.def_add_succ_l [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.def_add_0_l [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.def_add_wd [instance, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.def_add [definition, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.even [definition, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.even_succ [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.even_0 [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.even_wd [instance, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half [definition, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_decrease [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_nz [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_lower_bound [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_upper_bound [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_double [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_1 [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_0 [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_aux_spec2 [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_aux_spec [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_aux_succ [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_aux_0 [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_wd [instance, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_aux_wd [instance, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_aux [definition, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.if_zero_succ [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.if_zero_0 [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.if_zero_wd [instance, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.if_zero [definition, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.log [definition, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.log_step [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.log_init [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.log_good_step [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.log_wd [instance, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.log_prewd [instance, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.ltb [definition, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.ltb_ge [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.ltb_lt [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.ltb_0_succ [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.ltb_0 [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.ltb_step [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.ltb_base [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.ltb_wd [instance, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.pow [definition, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.pow_succ [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.pow_0 [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.pow_wd [instance, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.pow2_log [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.succ_ltb_mono [lemma, in Coq.Numbers.Natural.Abstract.NDefOps]
_ ^^ _ [notation, in Coq.Numbers.Natural.Abstract.NDefOps]
_ << _ [notation, in Coq.Numbers.Natural.Abstract.NDefOps]
_ ** _ [notation, in Coq.Numbers.Natural.Abstract.NDefOps]
_ +++ _ [notation, in Coq.Numbers.Natural.Abstract.NDefOps]
Ndiff_semantics [lemma, in Coq.NArith.Ndigits]
Ndigits [library]
Ndist [library]
NDiv [library]
Ndivide [abbreviation, in Coq.NArith.Ngcd_def]
NDivProp [module, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.add_mod [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.add_mod_idemp_r [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.add_mod_idemp_l [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_mul_le [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_div [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_mul_cancel_l [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_mul_cancel_r [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_add_l [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_add [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_le_compat_l [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_le_lower_bound [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_le_upper_bound [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_lt_upper_bound [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_exact [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_le_mono [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_lt [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_str_pos_iff [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_small_iff [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_str_pos [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_mul [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_1_l [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_1_r [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_0_l [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_small [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_same [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_unique_exact [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_unique [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_mod_unique [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_divides [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_mul_r [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_mod [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_add [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_small_iff [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_le [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_mul [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_1_l [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_1_r [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_0_l [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_small [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_same [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_unique [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_eq [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_upper_bound [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mul_mod [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mul_mod_idemp_r [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mul_mod_idemp_l [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mul_mod_distr_l [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mul_mod_distr_r [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mul_succ_div_gt [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mul_div_le [lemma, in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.Private_NZDiv [module, in Coq.Numbers.Natural.Abstract.NDiv]
NDivSpecific [module, in Coq.Numbers.Natural.Abstract.NAxioms]
NDivSpecific.mod_upper_bound [axiom, in Coq.Numbers.Natural.Abstract.NAxioms]
Ndiv_mod_eq [abbreviation, in Coq.NArith.Ndiv_def]
Ndiv_eucl_correct [abbreviation, in Coq.NArith.Ndiv_def]
Ndiv_Zquot [abbreviation, in Coq.ZArith.Zquot]
Ndiv_def [library]
Ndiv2_correct [lemma, in Coq.NArith.Ndigits]
Ndiv2_double_plus_one [lemma, in Coq.NArith.Ndigits]
Ndiv2_double [lemma, in Coq.NArith.Ndigits]
Ndiv2_bit_neq [lemma, in Coq.NArith.Ndec]
Ndiv2_bit_eq [lemma, in Coq.NArith.Ndec]
Ndiv2_neq [lemma, in Coq.NArith.Ndec]
Ndiv2_eq [lemma, in Coq.NArith.Ndec]
Ndouble_plus_one_bit0 [lemma, in Coq.NArith.Ndigits]
Ndouble_bit0 [lemma, in Coq.NArith.Ndigits]
Ndouble_plus_one_inj [abbreviation, in Coq.NArith.BinNat]
Ndouble_plus_one_div2 [abbreviation, in Coq.NArith.BinNat]
Ndouble_div2 [abbreviation, in Coq.NArith.BinNat]
Ndouble_plus_one [abbreviation, in Coq.NArith.BinNat]
Ndouble_or_double_plus_un [lemma, in Coq.NArith.Ndec]
neg [projection, in Coq.Reals.RIneq]
Neg [constructor, in Coq.Init.Decimal]
negate [definition, in Coq.micromega.ZMicromega]
negate [definition, in Coq.micromega.RingMicromega]
negate_correct [lemma, in Coq.micromega.ZMicromega]
negate_correct [lemma, in Coq.micromega.RingMicromega]
negative_derivative [lemma, in Coq.Reals.MVT]
negb [definition, in Coq.Init.Datatypes]
negbE [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
negbF [lemma, in Coq.ssr.ssrbool]
negbFE [lemma, in Coq.ssr.ssrbool]
negbK [lemma, in Coq.ssr.ssrbool]
negbLR [lemma, in Coq.ssr.ssrbool]
negbNE [lemma, in Coq.ssr.ssrbool]
negbRL [lemma, in Coq.ssr.ssrbool]
negbT [lemma, in Coq.ssr.ssrbool]
negbTE [lemma, in Coq.ssr.ssrbool]
negb_imply [lemma, in Coq.ssr.ssrbool]
negb_or [lemma, in Coq.ssr.ssrbool]
negb_and [lemma, in Coq.ssr.ssrbool]
negb_inj [lemma, in Coq.ssr.ssrbool]
negb_if [lemma, in Coq.Bool.Bool]
negb_prop_involutive [lemma, in Coq.Bool.Bool]
negb_prop_classical [lemma, in Coq.Bool.Bool]
negb_prop_intro [lemma, in Coq.Bool.Bool]
negb_prop_elim [lemma, in Coq.Bool.Bool]
negb_xorb_r [lemma, in Coq.Bool.Bool]
negb_xorb_l [lemma, in Coq.Bool.Bool]
negb_false_iff [lemma, in Coq.Bool.Bool]
negb_true_iff [lemma, in Coq.Bool.Bool]
negb_sym [lemma, in Coq.Bool.Bool]
negb_intro [abbreviation, in Coq.Bool.Bool]
negb_elim [abbreviation, in Coq.Bool.Bool]
negb_involutive_reverse [lemma, in Coq.Bool.Bool]
negb_involutive [lemma, in Coq.Bool.Bool]
negb_andb [lemma, in Coq.Bool.Bool]
negb_orb [lemma, in Coq.Bool.Bool]
negP [lemma, in Coq.ssr.ssrbool]
negPf [lemma, in Coq.ssr.ssrbool]
negPn [lemma, in Coq.ssr.ssrbool]
negreal [record, in Coq.Reals.RIneq]
neg_false [lemma, in Coq.Init.Logic]
neg_pos_Rsqr_le [lemma, in Coq.Reals.R_sqr]
neg_sin [lemma, in Coq.Reals.Rtrigo1]
neg_cos [lemma, in Coq.Reals.Rtrigo1]
neg_Forall_Exists_neg [lemma, in Coq.Lists.List]
neighbourhood [definition, in Coq.Reals.Rtopology]
neighbourhood_P1 [lemma, in Coq.Reals.Rtopology]
neq [definition, in Coq.ZArith.Znat]
Neqb_ok [lemma, in Coq.setoid_ring.InitialRing]
Neqb_complete [lemma, in Coq.NArith.Ndec]
Neqb_Ncompare [lemma, in Coq.NArith.Ndec]
Neqb_comm [abbreviation, in Coq.NArith.Ndec]
Neqb_correct [abbreviation, in Coq.NArith.Ndec]
Neqe [lemma, in Coq.setoid_ring.InitialRing]
nequiv_equiv_trans [lemma, in Coq.Classes.SetoidClass]
nequiv_decb [definition, in Coq.Classes.SetoidDec]
nequiv_dec [definition, in Coq.Classes.SetoidDec]
nequiv_decb [definition, in Coq.Classes.EquivDec]
nequiv_dec [definition, in Coq.Classes.EquivDec]
neq_O_lt [abbreviation, in Coq.Arith.Lt]
neq_0_lt [lemma, in Coq.Arith.Lt]
nesym [definition, in Coq.ssr.ssrfun]
Neven [definition, in Coq.NArith.Ndigits]
Neven_not_double_plus_one [lemma, in Coq.NArith.Ndec]
Newman [lemma, in Coq.Sets.Relations_3_facts]
NewtonInt [definition, in Coq.Reals.NewtonInt]
NewtonInt [library]
NewtonInt_P9 [lemma, in Coq.Reals.NewtonInt]
NewtonInt_P8 [lemma, in Coq.Reals.NewtonInt]
NewtonInt_P7 [lemma, in Coq.Reals.NewtonInt]
NewtonInt_P6 [lemma, in Coq.Reals.NewtonInt]
NewtonInt_P5 [lemma, in Coq.Reals.NewtonInt]
NewtonInt_P4 [lemma, in Coq.Reals.NewtonInt]
NewtonInt_P3 [lemma, in Coq.Reals.NewtonInt]
NewtonInt_P2 [lemma, in Coq.Reals.NewtonInt]
NewtonInt_P1 [lemma, in Coq.Reals.NewtonInt]
Newton_integrable [definition, in Coq.Reals.NewtonInt]
new_var [lemma, in Coq.omega.OmegaLemmas]
next [constructor, in Coq.Logic.ConstructiveEpsilon]
NExtraProp [module, in Coq.Numbers.Natural.Abstract.NProperties]
next_right [constructor, in Coq.Logic.WKL]
next_left [constructor, in Coq.Logic.WKL]
nfold [definition, in Coq.Numbers.NaryFunctions]
nfold_list [definition, in Coq.Numbers.NaryFunctions]
nfold_bis [definition, in Coq.Numbers.NaryFunctions]
NFormula [definition, in Coq.micromega.RingMicromega]
nformula_of_cutting_plane [definition, in Coq.micromega.ZMicromega]
nformula_plus_nformula_correct [lemma, in Coq.micromega.RingMicromega]
nformula_times_nformula_correct [lemma, in Coq.micromega.RingMicromega]
nformula_plus_nformula [definition, in Coq.micromega.RingMicromega]
nformula_times_nformula [definition, in Coq.micromega.RingMicromega]
nfun [definition, in Coq.Numbers.NaryFunctions]
nfun_to_nfun_bis [definition, in Coq.Numbers.NaryFunctions]
nfun_to_nfun [definition, in Coq.Numbers.NaryFunctions]
Ngcd [abbreviation, in Coq.NArith.Ngcd_def]
NGcd [library]
NGcdProp [module, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.Bezout [definition, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.bezout_1_gcd [lemma, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.Bezout_wd [instance, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_mul_split [lemma, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_gcd_iff' [definition, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_sub_r [lemma, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_add_cancel_r [lemma, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_antisym [definition, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_1_r [definition, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gauss [lemma, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_mul_mono_r [lemma, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_mul_mono_l [lemma, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_bezout [lemma, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_bezout_pos [lemma, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_bezout_pos_pos [lemma, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_sub_diag_r [lemma, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_add_diag_r [lemma, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_add_mult_diag_r [lemma, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_unique_alt' [definition, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_unique' [definition, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_diag [definition, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_0_r [definition, in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_0_l [definition, in Coq.Numbers.Natural.Abstract.NGcd]
Ngcd_greatest [abbreviation, in Coq.NArith.Ngcd_def]
Ngcd_divide_r [abbreviation, in Coq.NArith.Ngcd_def]
Ngcd_divide_l [abbreviation, in Coq.NArith.Ngcd_def]
Ngcd_def [library]
Nggcd [abbreviation, in Coq.NArith.Ngcd_def]
Nggcd_correct_divisors [abbreviation, in Coq.NArith.Ngcd_def]
Nggcd_gcd [abbreviation, in Coq.NArith.Ngcd_def]
Ngt_Nlt [abbreviation, in Coq.NArith.BinNat]
nhyps_of_psatz_correct [lemma, in Coq.micromega.RingMicromega]
nhyps_of_psatz [definition, in Coq.micromega.RingMicromega]
ni [constructor, in Coq.NArith.Ndist]
nil [constructor, in Coq.Reals.RList]
Nil [constructor, in Coq.Init.Decimal]
nil [constructor, in Coq.Init.Datatypes]
nil [constructor, in Coq.Vectors.VectorDef]
nil [abbreviation, in Coq.Lists.List]
NilEmpty [module, in Coq.Numbers.DecimalString]
NilEmpty.int_of_string [definition, in Coq.Numbers.DecimalString]
NilEmpty.isi [lemma, in Coq.Numbers.DecimalString]
NilEmpty.sis [lemma, in Coq.Numbers.DecimalString]
NilEmpty.string_of_int [definition, in Coq.Numbers.DecimalString]
NilEmpty.string_of_uint [definition, in Coq.Numbers.DecimalString]
NilEmpty.sus [lemma, in Coq.Numbers.DecimalString]
NilEmpty.uint_of_string [definition, in Coq.Numbers.DecimalString]
NilEmpty.usu [lemma, in Coq.Numbers.DecimalString]
NilZero [module, in Coq.Numbers.DecimalString]
NilZero.int_of_string [definition, in Coq.Numbers.DecimalString]
NilZero.isi [lemma, in Coq.Numbers.DecimalString]
NilZero.isi_negnil [lemma, in Coq.Numbers.DecimalString]
NilZero.isi_posnil [lemma, in Coq.Numbers.DecimalString]
NilZero.sis [lemma, in Coq.Numbers.DecimalString]
NilZero.string_of_int [definition, in Coq.Numbers.DecimalString]
NilZero.string_of_uint [definition, in Coq.Numbers.DecimalString]
NilZero.sus [lemma, in Coq.Numbers.DecimalString]
NilZero.uint_of_string_nonnil [lemma, in Coq.Numbers.DecimalString]
NilZero.uint_of_string [definition, in Coq.Numbers.DecimalString]
NilZero.usu [lemma, in Coq.Numbers.DecimalString]
NilZero.usu_gen [lemma, in Coq.Numbers.DecimalString]
NilZero.usu_nil [lemma, in Coq.Numbers.DecimalString]
nil_sort [abbreviation, in Coq.Sorting.Sorted]
nil_leA [abbreviation, in Coq.Sorting.Sorted]
nil_is_heap [constructor, in Coq.Sorting.Heap]
nil_cons [lemma, in Coq.Lists.List]
Nind [abbreviation, in Coq.NArith.BinNat]
Ninterp_PElist [abbreviation, in Coq.setoid_ring.Field_theory]
NIso [library]
ni_le_le [lemma, in Coq.NArith.Ndist]
ni_le_min_induc [lemma, in Coq.NArith.Ndist]
ni_le_total [lemma, in Coq.NArith.Ndist]
ni_min_case [lemma, in Coq.NArith.Ndist]
ni_le_min_2 [lemma, in Coq.NArith.Ndist]
ni_le_min_1 [lemma, in Coq.NArith.Ndist]
ni_le_trans [lemma, in Coq.NArith.Ndist]
ni_le_antisym [lemma, in Coq.NArith.Ndist]
ni_le_refl [lemma, in Coq.NArith.Ndist]
ni_le [definition, in Coq.NArith.Ndist]
ni_min_inf_r [lemma, in Coq.NArith.Ndist]
ni_min_inf_l [lemma, in Coq.NArith.Ndist]
ni_min_O_r [lemma, in Coq.NArith.Ndist]
ni_min_O_l [lemma, in Coq.NArith.Ndist]
ni_min_assoc [lemma, in Coq.NArith.Ndist]
ni_min_comm [lemma, in Coq.NArith.Ndist]
ni_min_idemp [lemma, in Coq.NArith.Ndist]
ni_min [definition, in Coq.NArith.Ndist]
NLcm [library]
NLcmProp [module, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.divide_lcm_iff [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.divide_lcm_eq_r [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.divide_div [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.divide_lcm_r [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.divide_lcm_l [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.divide_div_mul_exact [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.gcd_1_lcm_mul [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.gcd_div_swap [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.gcd_mod [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.gcd_div_gcd [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.gcd_div_factor [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm [definition, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_mul_mono_r [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_mul_mono_l [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_eq_0 [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_diag [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_1_r [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_1_l [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_0_r [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_0_l [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_assoc [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_unique_alt [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_unique [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_divide_iff [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_comm [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_least [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_equiv2 [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_equiv1 [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_wd [instance, in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.mod_divide [lemma, in Coq.Numbers.Natural.Abstract.NLcm]
Nleb [definition, in Coq.NArith.Ndec]
Nleb_double_plus_one_mono_conv [lemma, in Coq.NArith.Ndec]
Nleb_double_mono_conv [lemma, in Coq.NArith.Ndec]
Nleb_double_plus_one_mono [lemma, in Coq.NArith.Ndec]
Nleb_double_mono [lemma, in Coq.NArith.Ndec]
Nleb_ltb_trans [lemma, in Coq.NArith.Ndec]
Nleb_trans [lemma, in Coq.NArith.Ndec]
Nleb_antisym [lemma, in Coq.NArith.Ndec]
Nleb_refl [lemma, in Coq.NArith.Ndec]
Nleb_Nle [lemma, in Coq.NArith.Ndec]
Nleb_alt [lemma, in Coq.NArith.Ndec]
Nless [definition, in Coq.NArith.Ndigits]
Nless_total [lemma, in Coq.NArith.Ndigits]
Nless_trans [lemma, in Coq.NArith.Ndigits]
Nless_z [lemma, in Coq.NArith.Ndigits]
Nless_def_4 [lemma, in Coq.NArith.Ndigits]
Nless_def_3 [lemma, in Coq.NArith.Ndigits]
Nless_def_2 [lemma, in Coq.NArith.Ndigits]
Nless_def_1 [lemma, in Coq.NArith.Ndigits]
Nless_not_refl [lemma, in Coq.NArith.Ndigits]
Nless_aux [definition, in Coq.NArith.Ndigits]
Nle_lteq [abbreviation, in Coq.NArith.BinNat]
Nle_0 [abbreviation, in Coq.NArith.BinNat]
NLog [library]
NLog2Prop [module, in Coq.Numbers.Natural.Abstract.NLog]
Nltb_Ncompare [lemma, in Coq.NArith.Ndec]
Nltb_double_plus_one_mono_conv [lemma, in Coq.NArith.Ndec]
Nltb_double_mono_conv [lemma, in Coq.NArith.Ndec]
Nltb_double_plus_one_mono [lemma, in Coq.NArith.Ndec]
Nltb_double_mono [lemma, in Coq.NArith.Ndec]
Nltb_leb_weak [lemma, in Coq.NArith.Ndec]
Nltb_trans [lemma, in Coq.NArith.Ndec]
Nltb_leb_trans [lemma, in Coq.NArith.Ndec]
Nlt_not_eq [abbreviation, in Coq.NArith.BinNat]
NMaxMin [library]
NMaxMinProp [module, in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.add_min_distr_r [lemma, in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.add_min_distr_l [lemma, in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.add_max_distr_r [lemma, in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.add_max_distr_l [lemma, in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.max_0_r [lemma, in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.max_0_l [lemma, in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.min_0_r [lemma, in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.min_0_l [lemma, in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.mul_min_distr_r [lemma, in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.mul_min_distr_l [lemma, in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.mul_max_distr_r [lemma, in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.mul_max_distr_l [lemma, in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.sub_min_distr_r [lemma, in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.sub_min_distr_l [lemma, in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.sub_max_distr_r [lemma, in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.sub_max_distr_l [lemma, in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.succ_min_distr [lemma, in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.succ_max_distr [lemma, in Coq.Numbers.Natural.Abstract.NMaxMin]
Nminus [abbreviation, in Coq.NArith.BinNat]
Nminus_succ_r [abbreviation, in Coq.NArith.BinNat]
Nminus_0_r [abbreviation, in Coq.NArith.BinNat]
Nminus_N0_Nle [abbreviation, in Coq.NArith.BinNat]
Nmin_lt_4 [lemma, in Coq.NArith.Ndec]
Nmin_lt_3 [lemma, in Coq.NArith.Ndec]
Nmin_le_5 [lemma, in Coq.NArith.Ndec]
Nmin_le_4 [lemma, in Coq.NArith.Ndec]
Nmin_le_3 [lemma, in Coq.NArith.Ndec]
Nmin_le_2 [lemma, in Coq.NArith.Ndec]
Nmin_le_1 [lemma, in Coq.NArith.Ndec]
Nmin_choice [abbreviation, in Coq.NArith.Ndec]
Nmk_monpol_list [abbreviation, in Coq.setoid_ring.Field_theory]
Nmod [abbreviation, in Coq.NArith.Ndiv_def]
Nmod_Zrem [abbreviation, in Coq.ZArith.Zquot]
NMORPHISM [section, in Coq.setoid_ring.InitialRing]
NMORPHISM.ARth [variable, in Coq.setoid_ring.InitialRing]
NMORPHISM.R [variable, in Coq.setoid_ring.InitialRing]
NMORPHISM.radd [variable, in Coq.setoid_ring.InitialRing]
NMORPHISM.req [variable, in Coq.setoid_ring.InitialRing]
NMORPHISM.Reqe [variable, in Coq.setoid_ring.InitialRing]
NMORPHISM.rI [variable, in Coq.setoid_ring.InitialRing]
NMORPHISM.rmul [variable, in Coq.setoid_ring.InitialRing]
NMORPHISM.rO [variable, in Coq.setoid_ring.InitialRing]
NMORPHISM.ropp [variable, in Coq.setoid_ring.InitialRing]
NMORPHISM.Rsth [variable, in Coq.setoid_ring.InitialRing]
NMORPHISM.rsub [variable, in Coq.setoid_ring.InitialRing]
NMORPHISM.SReqe [variable, in Coq.setoid_ring.InitialRing]
NMORPHISM.SRth [variable, in Coq.setoid_ring.InitialRing]
_ == _ [notation, in Coq.setoid_ring.InitialRing]
_ - _ [notation, in Coq.setoid_ring.InitialRing]
_ * _ [notation, in Coq.setoid_ring.InitialRing]
_ + _ [notation, in Coq.setoid_ring.InitialRing]
- _ [notation, in Coq.setoid_ring.InitialRing]
0 [notation, in Coq.setoid_ring.InitialRing]
1 [notation, in Coq.setoid_ring.InitialRing]
[ _ ] [notation, in Coq.setoid_ring.InitialRing]
NMulOrder [library]
NMulOrderProp [module, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.eq_mul_1 [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.lt_0_mul' [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.mul_eq_1 [definition, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.mul_pos [abbreviation, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.mul_le_mono [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.mul_lt_mono [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.mul_le_mono_r [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.mul_le_mono_l [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.square_le_mono [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.square_lt_mono [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
Nmult [abbreviation, in Coq.NArith.BinNat]
Nmult_reg_r [lemma, in Coq.NArith.BinNat]
Nmult_plus_distr_l [lemma, in Coq.NArith.BinNat]
Nmult_Sn_m [lemma, in Coq.NArith.BinNat]
Nmult_plus_distr_r [abbreviation, in Coq.NArith.BinNat]
Nmult_assoc [abbreviation, in Coq.NArith.BinNat]
Nmult_comm [abbreviation, in Coq.NArith.BinNat]
Nmult_1_r [abbreviation, in Coq.NArith.BinNat]
Nmult_1_l [abbreviation, in Coq.NArith.BinNat]
Nmult_0_l [abbreviation, in Coq.NArith.BinNat]
Nnat [library]
Nneg_bit0_2 [lemma, in Coq.NArith.Ndigits]
Nneg_bit0_1 [lemma, in Coq.NArith.Ndigits]
Nneg_bit0 [lemma, in Coq.NArith.Ndigits]
Nneq_elim [lemma, in Coq.NArith.Ndec]
Nnorm [abbreviation, in Coq.setoid_ring.Field_theory]
Nnot_div2_not_double_plus_one [lemma, in Coq.NArith.Ndec]
Nnot_div2_not_double [lemma, in Coq.NArith.Ndec]
NNPP [lemma, in Coq.Logic.Classical_Prop]
Nodd [definition, in Coq.NArith.Ndigits]
Nodd_not_double [lemma, in Coq.NArith.Ndec]
node [definition, in Coq.micromega.ZMicromega]
NodepOfDep [module, in Coq.FSets.FSetBridge]
NodepOfDep.Add [definition, in Coq.FSets.FSetBridge]
NodepOfDep.add [definition, in Coq.FSets.FSetBridge]
NodepOfDep.add_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.add_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.add_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.cardinal [definition, in Coq.FSets.FSetBridge]
NodepOfDep.cardinal_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.choose [definition, in Coq.FSets.FSetBridge]
NodepOfDep.choose_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.choose_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.choose_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.compare [definition, in Coq.FSets.FSetBridge]
NodepOfDep.compat_P_aux [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.diff [definition, in Coq.FSets.FSetBridge]
NodepOfDep.diff_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.diff_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.diff_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.E [module, in Coq.FSets.FSetBridge]
NodepOfDep.elements [definition, in Coq.FSets.FSetBridge]
NodepOfDep.elements_3w [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.elements_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.elements_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.elements_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.elt [definition, in Coq.FSets.FSetBridge]
NodepOfDep.Empty [definition, in Coq.FSets.FSetBridge]
NodepOfDep.empty [definition, in Coq.FSets.FSetBridge]
NodepOfDep.empty_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.eq [definition, in Coq.FSets.FSetBridge]
NodepOfDep.Equal [definition, in Coq.FSets.FSetBridge]
NodepOfDep.equal [definition, in Coq.FSets.FSetBridge]
NodepOfDep.equal_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.equal_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.eq_trans [definition, in Coq.FSets.FSetBridge]
NodepOfDep.eq_sym [definition, in Coq.FSets.FSetBridge]
NodepOfDep.eq_refl [definition, in Coq.FSets.FSetBridge]
NodepOfDep.eq_dec [definition, in Coq.FSets.FSetBridge]
NodepOfDep.Exists [definition, in Coq.FSets.FSetBridge]
NodepOfDep.exists_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.exists_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.exists_ [definition, in Coq.FSets.FSetBridge]
NodepOfDep.filter [definition, in Coq.FSets.FSetBridge]
NodepOfDep.filter_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.filter_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.filter_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.fold [definition, in Coq.FSets.FSetBridge]
NodepOfDep.fold_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.For_all [definition, in Coq.FSets.FSetBridge]
NodepOfDep.for_all_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.for_all_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.for_all [definition, in Coq.FSets.FSetBridge]
NodepOfDep.f_dec [definition, in Coq.FSets.FSetBridge]
NodepOfDep.In [definition, in Coq.FSets.FSetBridge]
NodepOfDep.inter [definition, in Coq.FSets.FSetBridge]
NodepOfDep.inter_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.inter_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.inter_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.In_1 [definition, in Coq.FSets.FSetBridge]
NodepOfDep.is_empty_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.is_empty_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.is_empty [definition, in Coq.FSets.FSetBridge]
NodepOfDep.lt [definition, in Coq.FSets.FSetBridge]
NodepOfDep.lt_not_eq [definition, in Coq.FSets.FSetBridge]
NodepOfDep.lt_trans [definition, in Coq.FSets.FSetBridge]
NodepOfDep.max_elt_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.max_elt_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.max_elt_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.max_elt [definition, in Coq.FSets.FSetBridge]
NodepOfDep.ME [module, in Coq.FSets.FSetBridge]
NodepOfDep.mem [definition, in Coq.FSets.FSetBridge]
NodepOfDep.mem_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.mem_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.min_elt_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.min_elt_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.min_elt_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.min_elt [definition, in Coq.FSets.FSetBridge]
NodepOfDep.partition [definition, in Coq.FSets.FSetBridge]
NodepOfDep.partition_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.partition_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.remove [definition, in Coq.FSets.FSetBridge]
NodepOfDep.remove_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.remove_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.remove_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.singleton [definition, in Coq.FSets.FSetBridge]
NodepOfDep.singleton_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.singleton_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.Subset [definition, in Coq.FSets.FSetBridge]
NodepOfDep.subset [definition, in Coq.FSets.FSetBridge]
NodepOfDep.subset_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.subset_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.t [definition, in Coq.FSets.FSetBridge]
NodepOfDep.union [definition, in Coq.FSets.FSetBridge]
NodepOfDep.union_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.union_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.union_1 [lemma, in Coq.FSets.FSetBridge]
node_is_heap [constructor, in Coq.Sorting.Heap]
nodup [definition, in Coq.Lists.List]
NoDup [inductive, in Coq.Lists.List]
NoDupA [inductive, in Coq.Lists.SetoidList]
NoDupA_equivlistA_permut [lemma, in Coq.Sorting.PermutSetoid]
NoDupA_equivlistA_decompose [lemma, in Coq.Lists.SetoidPermutation]
NoDupA_equivlistA_PermutationA [lemma, in Coq.Lists.SetoidPermutation]
NoDupA_singleton [lemma, in Coq.Lists.SetoidList]
NoDupA_swap [lemma, in Coq.Lists.SetoidList]
NoDupA_split [lemma, in Coq.Lists.SetoidList]
NoDupA_rev [lemma, in Coq.Lists.SetoidList]
NoDupA_app [lemma, in Coq.Lists.SetoidList]
NoDupA_altdef [lemma, in Coq.Lists.SetoidList]
NoDupA_cons [constructor, in Coq.Lists.SetoidList]
NoDupA_nil [constructor, in Coq.Lists.SetoidList]
NoDup_permut [lemma, in Coq.Sorting.PermutEq]
NoDup_dec [lemma, in Coq.Lists.ListDec]
NoDup_decidable [lemma, in Coq.Lists.ListDec]
NoDup_Permutation_bis [lemma, in Coq.Sorting.Permutation]
NoDup_Permutation [lemma, in Coq.Sorting.Permutation]
NoDup_map_inv [lemma, in Coq.Lists.List]
NoDup_length_incl [lemma, in Coq.Lists.List]
NoDup_incl_length [lemma, in Coq.Lists.List]
NoDup_nth [lemma, in Coq.Lists.List]
NoDup_nth_error [lemma, in Coq.Lists.List]
NoDup_count_occ' [lemma, in Coq.Lists.List]
NoDup_count_occ [lemma, in Coq.Lists.List]
nodup_inv [lemma, in Coq.Lists.List]
NoDup_nodup [lemma, in Coq.Lists.List]
nodup_In [lemma, in Coq.Lists.List]
NoDup_cons_iff [lemma, in Coq.Lists.List]
NoDup_remove_2 [lemma, in Coq.Lists.List]
NoDup_remove_1 [lemma, in Coq.Lists.List]
NoDup_remove [lemma, in Coq.Lists.List]
NoDup_Add [lemma, in Coq.Lists.List]
NoDup_cons [constructor, in Coq.Lists.List]
NoDup_nil [constructor, in Coq.Lists.List]
Noetherian [definition, in Coq.Sets.Relations_3]
noetherian [inductive, in Coq.Sets.Relations_3]
Noetherian_contains_Noetherian [lemma, in Coq.Sets.Relations_3_facts]
None [constructor, in Coq.Init.Datatypes]
NonEqual [constructor, in Coq.micromega.RingMicromega]
nonneg [projection, in Coq.Reals.RIneq]
nonnegreal [record, in Coq.Reals.RIneq]
nonneg_derivative_0 [lemma, in Coq.Reals.Ranalysis1]
nonneg_derivative_1 [lemma, in Coq.Reals.MVT]
nonpos [projection, in Coq.Reals.RIneq]
nonposreal [record, in Coq.Reals.RIneq]
nonpos_derivative_1 [lemma, in Coq.Reals.MVT]
nonpos_derivative_0 [lemma, in Coq.Reals.MVT]
NonPropType [module, in Coq.ssr.ssreflect]
NonPropType.call [definition, in Coq.ssr.ssreflect]
NonPropType.Call [constructor, in Coq.ssr.ssreflect]
NonPropType.callee [projection, in Coq.ssr.ssreflect]
NonPropType.call_of [record, in Coq.ssr.ssreflect]
NonPropType.check [definition, in Coq.ssr.ssreflect]
NonPropType.Check [constructor, in Coq.ssr.ssreflect]
NonPropType.condition [projection, in Coq.ssr.ssreflect]
NonPropType.Exports [module, in Coq.ssr.ssreflect]
NonPropType.Exports.nonPropType [abbreviation, in Coq.ssr.ssreflect]
NonPropType.Exports.notProp [abbreviation, in Coq.ssr.ssreflect]
NonPropType.frame [projection, in Coq.ssr.ssreflect]
NonPropType.maybeProp [definition, in Coq.ssr.ssreflect]
NonPropType.result [projection, in Coq.ssr.ssreflect]
NonPropType.test [projection, in Coq.ssr.ssreflect]
NonPropType.Test [constructor, in Coq.ssr.ssreflect]
NonPropType.test_negative [definition, in Coq.ssr.ssreflect]
NonPropType.test_Prop [definition, in Coq.ssr.ssreflect]
NonPropType.test_of [record, in Coq.ssr.ssreflect]
NonPropType.type [record, in Coq.ssr.ssreflect]
NonStrict [constructor, in Coq.micromega.RingMicromega]
nonzero [projection, in Coq.Reals.RIneq]
nonzeroreal [record, in Coq.Reals.RIneq]
non_dep_dep_functional_rel_reification [lemma, in Coq.Logic.ChoiceFacts]
non_dep_dep_functional_choice [lemma, in Coq.Logic.ChoiceFacts]
Non_disjoint_union' [lemma, in Coq.Sets.Powerset_facts]
Non_disjoint_union [lemma, in Coq.Sets.Powerset_facts]
Noone_in_empty [lemma, in Coq.Sets.Constructive_sets]
Nop [module, in Coq.Structures.Equalities]
Nopp [definition, in Coq.setoid_ring.InitialRing]
NOrder [library]
NOrderProp [module, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.eq_0_gt_0_cases [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.le_pred_le_succ [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.le_succ_le_pred [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.le_pred_le [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.le_le_pred [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.le_pred_l [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.le_ind_rel [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.le_1_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.le_0_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_pred_lt_succ [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_succ_lt_pred [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_pred_lt [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_pred_le [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_le_pred [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_lt_pred [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_pred_l [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_ind_rel [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_1_l' [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_lt_0 [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_1_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_0_succ [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_wf_0 [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.neq_0_lt_0 [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.nle_succ_0 [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.nlt_0_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.pred_lt_mono [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.pred_le_mono [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.RelElim [section, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.RelElim.R [variable, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.RelElim.R_wd [variable, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.succ_pred_pos [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.zero_one [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NoRetractFromSmallPropositionToProp [module, in Coq.Logic.Hurkens]
NoRetractFromSmallPropositionToProp.El [definition, in Coq.Logic.Hurkens]
NoRetractFromSmallPropositionToProp.mparadox [lemma, in Coq.Logic.Hurkens]
NoRetractFromSmallPropositionToProp.MParadox [section, in Coq.Logic.Hurkens]
NoRetractFromSmallPropositionToProp.MParadox.bool [variable, in Coq.Logic.Hurkens]
NoRetractFromSmallPropositionToProp.MParadox.b2p [variable, in Coq.Logic.Hurkens]
NoRetractFromSmallPropositionToProp.MParadox.p2b [variable, in Coq.Logic.Hurkens]
NoRetractFromSmallPropositionToProp.MParadox.p2p1 [variable, in Coq.Logic.Hurkens]
NoRetractFromSmallPropositionToProp.MParadox.p2p2 [variable, in Coq.Logic.Hurkens]
NoRetractFromSmallPropositionToProp.NProp [definition, in Coq.Logic.Hurkens]
NoRetractFromSmallPropositionToProp.paradox [lemma, in Coq.Logic.Hurkens]
NoRetractFromSmallPropositionToProp.Paradox [section, in Coq.Logic.Hurkens]
NoRetractFromSmallPropositionToProp.Paradox.bool [variable, in Coq.Logic.Hurkens]
NoRetractFromSmallPropositionToProp.Paradox.b2p [variable, in Coq.Logic.Hurkens]
NoRetractFromSmallPropositionToProp.Paradox.p2b [variable, in Coq.Logic.Hurkens]
NoRetractFromSmallPropositionToProp.Paradox.p2p1 [variable, in Coq.Logic.Hurkens]
NoRetractFromSmallPropositionToProp.Paradox.p2p2 [variable, in Coq.Logic.Hurkens]
NoRetractFromTypeToProp [module, in Coq.Logic.Hurkens]
NoRetractFromTypeToProp.paradox [lemma, in Coq.Logic.Hurkens]
NoRetractFromTypeToProp.Paradox [section, in Coq.Logic.Hurkens]
NoRetractFromTypeToProp.Paradox.down [variable, in Coq.Logic.Hurkens]
NoRetractFromTypeToProp.Paradox.up [variable, in Coq.Logic.Hurkens]
NoRetractFromTypeToProp.Paradox.up_down [variable, in Coq.Logic.Hurkens]
NoRetractFromTypeToProp.Type1 [definition, in Coq.Logic.Hurkens]
NoRetractFromTypeToProp.Type2 [definition, in Coq.Logic.Hurkens]
NoRetractToImpredicativeUniverse [module, in Coq.Logic.Hurkens]
NoRetractToImpredicativeUniverse.paradox [lemma, in Coq.Logic.Hurkens]
NoRetractToImpredicativeUniverse.Paradox [section, in Coq.Logic.Hurkens]
NoRetractToImpredicativeUniverse.Paradox.U0 [variable, in Coq.Logic.Hurkens]
NoRetractToImpredicativeUniverse.Paradox.u02u1 [variable, in Coq.Logic.Hurkens]
NoRetractToImpredicativeUniverse.Paradox.U1 [variable, in Coq.Logic.Hurkens]
NoRetractToImpredicativeUniverse.Paradox.u12u0 [variable, in Coq.Logic.Hurkens]
NoRetractToImpredicativeUniverse.Paradox.u12u0_counit [variable, in Coq.Logic.Hurkens]
NoRetractToImpredicativeUniverse.Paradox.u12u0_unit [variable, in Coq.Logic.Hurkens]
NoRetractToImpredicativeUniverse.Paradox.U2 [variable, in Coq.Logic.Hurkens]
NoRetractToImpredicativeUniverse.Paradox.u22u1 [variable, in Coq.Logic.Hurkens]
NoRetractToImpredicativeUniverse.Paradox.u22u1_coherent [variable, in Coq.Logic.Hurkens]
NoRetractToImpredicativeUniverse.Paradox.u22u1_counit [variable, in Coq.Logic.Hurkens]
NoRetractToImpredicativeUniverse.Paradox.u22u1_unit [variable, in Coq.Logic.Hurkens]
NoRetractToModalProposition [module, in Coq.Logic.Hurkens]
NoRetractToModalProposition.El [definition, in Coq.Logic.Hurkens]
NoRetractToModalProposition.Forall [definition, in Coq.Logic.Hurkens]
NoRetractToModalProposition.modal [lemma, in Coq.Logic.Hurkens]
NoRetractToModalProposition.MProp [definition, in Coq.Logic.Hurkens]
NoRetractToModalProposition.paradox [lemma, in Coq.Logic.Hurkens]
NoRetractToModalProposition.Paradox [section, in Coq.Logic.Hurkens]
NoRetractToModalProposition.Paradox.bool [variable, in Coq.Logic.Hurkens]
NoRetractToModalProposition.Paradox.b2p [variable, in Coq.Logic.Hurkens]
NoRetractToModalProposition.Paradox.incr [variable, in Coq.Logic.Hurkens]
NoRetractToModalProposition.Paradox.M [variable, in Coq.Logic.Hurkens]
NoRetractToModalProposition.Paradox.p2b [variable, in Coq.Logic.Hurkens]
NoRetractToModalProposition.Paradox.p2p1 [variable, in Coq.Logic.Hurkens]
NoRetractToModalProposition.Paradox.p2p2 [variable, in Coq.Logic.Hurkens]
NoRetractToModalProposition.strength [lemma, in Coq.Logic.Hurkens]
NoRetractToNegativeProp [module, in Coq.Logic.Hurkens]
NoRetractToNegativeProp.El [definition, in Coq.Logic.Hurkens]
NoRetractToNegativeProp.NProp [definition, in Coq.Logic.Hurkens]
NoRetractToNegativeProp.paradox [lemma, in Coq.Logic.Hurkens]
NoRetractToNegativeProp.Paradox [section, in Coq.Logic.Hurkens]
NoRetractToNegativeProp.Paradox.bool [variable, in Coq.Logic.Hurkens]
NoRetractToNegativeProp.Paradox.b2p [variable, in Coq.Logic.Hurkens]
NoRetractToNegativeProp.Paradox.p2b [variable, in Coq.Logic.Hurkens]
NoRetractToNegativeProp.Paradox.p2p1 [variable, in Coq.Logic.Hurkens]
NoRetractToNegativeProp.Paradox.p2p2 [variable, in Coq.Logic.Hurkens]
norm [definition, in Coq.Init.Decimal]
norm [definition, in Coq.micromega.RingMicromega]
norm [definition, in Coq.nsatz.Nsatz]
normalise [definition, in Coq.micromega.ZMicromega]
normalise [definition, in Coq.micromega.RingMicromega]
normalise_correct [lemma, in Coq.micromega.ZMicromega]
normalise_sound [lemma, in Coq.micromega.RingMicromega]
normalization_done [inductive, in Coq.Classes.Morphisms]
normalization_done [inductive, in Coq.Classes.CMorphisms]
Normalize [section, in Coq.Classes.Morphisms]
Normalize [section, in Coq.Classes.CMorphisms]
normalizes [projection, in Coq.Classes.Morphisms]
Normalizes [record, in Coq.Classes.Morphisms]
normalizes [constructor, in Coq.Classes.Morphisms]
Normalizes [inductive, in Coq.Classes.Morphisms]
normalizes [projection, in Coq.Classes.CMorphisms]
Normalizes [record, in Coq.Classes.CMorphisms]
normalizes [constructor, in Coq.Classes.CMorphisms]
Normalizes [inductive, in Coq.Classes.CMorphisms]
normQ [definition, in Coq.micromega.QMicromega]
normZ [definition, in Coq.micromega.ZMicromega]
norm_aux_spec [lemma, in Coq.micromega.EnvRing]
norm_aux_PEopp [lemma, in Coq.micromega.EnvRing]
norm_aux_PEadd [lemma, in Coq.micromega.EnvRing]
norm_subst [definition, in Coq.micromega.EnvRing]
norm_aux [definition, in Coq.micromega.EnvRing]
norm_invol [lemma, in Coq.Numbers.DecimalFacts]
norm_subst_ok [lemma, in Coq.setoid_ring.Ncring_polynom]
norm_subst_spec [lemma, in Coq.setoid_ring.Ncring_polynom]
norm_aux_spec [lemma, in Coq.setoid_ring.Ncring_polynom]
norm_subst [definition, in Coq.setoid_ring.Ncring_polynom]
norm_aux [definition, in Coq.setoid_ring.Ncring_polynom]
norm_correct [lemma, in Coq.nsatz.Nsatz]
norm_subst_ok [lemma, in Coq.setoid_ring.Ring_polynom]
norm_subst_spec [lemma, in Coq.setoid_ring.Ring_polynom]
norm_aux_spec [lemma, in Coq.setoid_ring.Ring_polynom]
norm_aux_PEopp [lemma, in Coq.setoid_ring.Ring_polynom]
norm_aux_PEadd [lemma, in Coq.setoid_ring.Ring_polynom]
norm_subst [definition, in Coq.setoid_ring.Ring_polynom]
norm_aux [definition, in Coq.setoid_ring.Ring_polynom]
norP [lemma, in Coq.ssr.ssrbool]
Nor_semantics [lemma, in Coq.NArith.Ndigits]
nosimpl [abbreviation, in Coq.ssr.ssreflect]
not [definition, in Coq.Init.Logic]
Notations [library]
NotConstant [definition, in Coq.setoid_ring.Ncring_initial]
NotConstant [definition, in Coq.setoid_ring.InitialRing]
notF [definition, in Coq.ssr.ssrbool]
notT [definition, in Coq.Init.Logic_Type]
notzerop [definition, in Coq.Arith.Bool_nat]
notzerop_bool [definition, in Coq.Arith.Bool_nat]
not_le_minus_0 [lemma, in Coq.Arith.Minus]
not_not_classic_set [lemma, in Coq.Logic.ClassicalUniqueChoice]
not_or_and [lemma, in Coq.Logic.Classical_Prop]
not_and_or [lemma, in Coq.Logic.Classical_Prop]
not_imply_elim2 [lemma, in Coq.Logic.Classical_Prop]
not_imply_elim [lemma, in Coq.Logic.Classical_Prop]
not_imp_rev_iff [lemma, in Coq.Logic.Decidable]
not_imp_iff [lemma, in Coq.Logic.Decidable]
not_and_iff [lemma, in Coq.Logic.Decidable]
not_or_iff [lemma, in Coq.Logic.Decidable]
not_not_iff [lemma, in Coq.Logic.Decidable]
not_false_iff [lemma, in Coq.Logic.Decidable]
not_true_iff [lemma, in Coq.Logic.Decidable]
not_iff [lemma, in Coq.Logic.Decidable]
not_imp [lemma, in Coq.Logic.Decidable]
not_and [lemma, in Coq.Logic.Decidable]
not_or [lemma, in Coq.Logic.Decidable]
not_not [lemma, in Coq.Logic.Decidable]
not_O_IZR [abbreviation, in Coq.Reals.RIneq]
not_O_INR [abbreviation, in Coq.Reals.RIneq]
not_INR_O [abbreviation, in Coq.Reals.RIneq]
not_nm_INR [abbreviation, in Coq.Reals.RIneq]
not_0_IZR [lemma, in Coq.Reals.RIneq]
not_1_INR [lemma, in Coq.Reals.RIneq]
not_INR [lemma, in Coq.Reals.RIneq]
not_0_INR [lemma, in Coq.Reals.RIneq]
not_Zne [lemma, in Coq.ZArith.Zorder]
not_Zeq [lemma, in Coq.ZArith.Zorder]
not_injective_elim [lemma, in Coq.Sets.Image]
not_ex_not_all [lemma, in Coq.Logic.Classical_Pred_Type]
not_ex_all_not [lemma, in Coq.Logic.Classical_Pred_Type]
not_all_ex_not [lemma, in Coq.Logic.Classical_Pred_Type]
not_all_not_ex [lemma, in Coq.Logic.Classical_Pred_Type]
not_eq_sym [lemma, in Coq.Init.Logic]
not_iff_compat [lemma, in Coq.Init.Logic]
not_eq_sym [abbreviation, in Coq.Arith.Compare]
not_SIncl_empty [lemma, in Coq.Sets.Classical_sets]
not_empty_Inhabited [lemma, in Coq.Sets.Classical_sets]
not_included_empty_Inhabited [lemma, in Coq.Sets.Classical_sets]
not_false_is_true [lemma, in Coq.ssr.ssrbool]
not_prime_divide [lemma, in Coq.ZArith.Znumtheory]
not_prime_1 [lemma, in Coq.ZArith.Znumtheory]
not_prime_0 [lemma, in Coq.ZArith.Znumtheory]
not_rel_prime_0 [lemma, in Coq.ZArith.Znumtheory]
not_not_archimedean [lemma, in Coq.Reals.Rlogic]
not_eq_false_beq [definition, in Coq.Bool.BoolEq]
not_Zeq_inf [lemma, in Coq.ZArith.ZArith_dec]
not_make_conj_app [lemma, in Coq.micromega.Refl]
not_make_conj_cons [lemma, in Coq.micromega.Refl]
not_has_fixpoint [lemma, in Coq.Logic.Berardi]
Not_b [definition, in Coq.Logic.Berardi]
not_Empty_Add [lemma, in Coq.Sets.Constructive_sets]
not_eq_S [lemma, in Coq.Init.Peano]
not_iff_morphism [instance, in Coq.Classes.Morphisms_Prop]
not_impl_morphism [instance, in Coq.Classes.Morphisms_Prop]
not_locked_false_eq_true [lemma, in Coq.ssr.ssreflect]
not_Rlt [lemma, in Coq.Reals.SeqProp]
not_identity_sym [lemma, in Coq.Init.Logic_Type]
not_even_and_odd [lemma, in Coq.Arith.Even]
not_false_iff_true [lemma, in Coq.Bool.Bool]
not_true_iff_false [lemma, in Coq.Bool.Bool]
not_false_is_true [lemma, in Coq.Bool.Bool]
not_true_is_false [lemma, in Coq.Bool.Bool]
not_in_cons [lemma, in Coq.Lists.List]
not_lt [lemma, in Coq.Arith.Compare_dec]
not_ge [lemma, in Coq.Arith.Compare_dec]
not_gt [lemma, in Coq.Arith.Compare_dec]
not_le [lemma, in Coq.Arith.Compare_dec]
not_eq [lemma, in Coq.Arith.Compare_dec]
now [constructor, in Coq.Logic.WeakFan]
now_at [constructor, in Coq.Logic.WKL]
no_cond [definition, in Coq.Reals.Ranalysis1]
no_middle_eval_tt [lemma, in Coq.micromega.Tauto]
no_fixpoint_negb [lemma, in Coq.Bool.Bool]
NParity [library]
NParityProp [module, in Coq.Numbers.Natural.Abstract.NParity]
NParityProp.even_sub [lemma, in Coq.Numbers.Natural.Abstract.NParity]
NParityProp.even_pred [lemma, in Coq.Numbers.Natural.Abstract.NParity]
NParityProp.odd_sub [lemma, in Coq.Numbers.Natural.Abstract.NParity]
NParityProp.odd_pred [lemma, in Coq.Numbers.Natural.Abstract.NParity]
Npdist [definition, in Coq.NArith.Ndist]
Npdist_ultra [lemma, in Coq.NArith.Ndist]
Npdist_comm [lemma, in Coq.NArith.Ndist]
Npdist_eq_2 [lemma, in Coq.NArith.Ndist]
Npdist_eq_1 [lemma, in Coq.NArith.Ndist]
NPEadd [definition, in Coq.setoid_ring.Field_theory]
NPEadd_ok [lemma, in Coq.setoid_ring.Field_theory]
NPeano [library]
NPEequiv [definition, in Coq.setoid_ring.Field_theory]
NPEequiv_eq [instance, in Coq.setoid_ring.Field_theory]
NPEeval [abbreviation, in Coq.setoid_ring.Field_theory]
NPEeval_ext [instance, in Coq.setoid_ring.Field_theory]
NPEmul [definition, in Coq.setoid_ring.Field_theory]
NPEmul_ok [lemma, in Coq.setoid_ring.Field_theory]
NPEopp [definition, in Coq.setoid_ring.Field_theory]
NPEopp_ok [lemma, in Coq.setoid_ring.Field_theory]
NPEpow [definition, in Coq.setoid_ring.Field_theory]
NPEpow_ok [lemma, in Coq.setoid_ring.Field_theory]
NPEsub [definition, in Coq.setoid_ring.Field_theory]
NPEsub_ok [lemma, in Coq.setoid_ring.Field_theory]
Nplength [definition, in Coq.NArith.Ndist]
Nplength_ultra [lemma, in Coq.NArith.Ndist]
Nplength_ultra_1 [lemma, in Coq.NArith.Ndist]
Nplength_ub [lemma, in Coq.NArith.Ndist]
Nplength_lb [lemma, in Coq.NArith.Ndist]
Nplength_first_one [lemma, in Coq.NArith.Ndist]
Nplength_one [lemma, in Coq.NArith.Ndist]
Nplength_zeros [lemma, in Coq.NArith.Ndist]
Nplength_infty [lemma, in Coq.NArith.Ndist]
Nplus [abbreviation, in Coq.NArith.BinNat]
Nplus_reg_l [lemma, in Coq.NArith.BinNat]
Nplus_succ [abbreviation, in Coq.NArith.BinNat]
Nplus_assoc [abbreviation, in Coq.NArith.BinNat]
Nplus_comm [abbreviation, in Coq.NArith.BinNat]
Nplus_0_r [abbreviation, in Coq.NArith.BinNat]
Nplus_0_l [abbreviation, in Coq.NArith.BinNat]
Npos [abbreviation, in Coq.NArith.BinNat]
Npos [constructor, in Coq.Numbers.BinNums]
NPow [library]
NPowProp [module, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.even_pow [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.odd_pow [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_add_upper [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_add_lower [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_gt_lin_r [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_le_mono_r_iff [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_lt_mono_r_iff [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_le_mono_l_iff [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_lt_mono_l_iff [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_inj_r [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_inj_l [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_lt_mono [definition, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_le_mono [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_le_mono_r [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_lt_mono_r [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_gt_1 [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_le_mono_l [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_lt_mono_l [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_eq_0_iff [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_nonzero [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_eq_0 [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_mul_r [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_mul_l [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_add_r [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_2_r [definition, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_1_l [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_1_r [definition, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_0_l [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_succ_r' [lemma, in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.Private_NZPow [module, in Coq.Numbers.Natural.Abstract.NPow]
NPphi_pow [abbreviation, in Coq.setoid_ring.Field_theory]
NPphi_dev [abbreviation, in Coq.setoid_ring.Field_theory]
Npred_minus [abbreviation, in Coq.NArith.BinNat]
nprod [definition, in Coq.Numbers.NaryFunctions]
nprod_of_list [definition, in Coq.Numbers.NaryFunctions]
nprod_to_list [definition, in Coq.Numbers.NaryFunctions]
NProp [abbreviation, in Coq.Logic.ClassicalFacts]
NProperties [library]
Nrec [abbreviation, in Coq.NArith.BinNat]
Nrect [abbreviation, in Coq.NArith.BinNat]
Nrect_step [abbreviation, in Coq.NArith.BinNat]
Nrect_base [abbreviation, in Coq.NArith.BinNat]
Nrec_succ [abbreviation, in Coq.NArith.BinNat]
Nrec_base [abbreviation, in Coq.NArith.BinNat]
Nsame_bit0 [lemma, in Coq.NArith.Ndigits]
Nsatz [library]
nsatzR_diff [lemma, in Coq.nsatz.Nsatz]
nsatz1 [section, in Coq.nsatz.Nsatz]
Nseqe [lemma, in Coq.setoid_ring.InitialRing]
nshiftl [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftl_above_size [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftl_size [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftl_n_0 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftl_S_tail [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftl_S [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Nshiftl_nat_spec_low [lemma, in Coq.NArith.Ndigits]
Nshiftl_nat_spec_high [lemma, in Coq.NArith.Ndigits]
Nshiftl_equiv_nat [lemma, in Coq.NArith.Ndigits]
Nshiftl_nat_equiv [lemma, in Coq.NArith.Ndigits]
Nshiftl_nat_S [lemma, in Coq.NArith.Ndigits]
nshiftr [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_0_firstl [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_0_propagates [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_predsize_0_firstl [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_above_size [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_size [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_n_0 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_S_tail [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_S [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Nshiftr_nat_spec [lemma, in Coq.NArith.Ndigits]
Nshiftr_equiv_nat [lemma, in Coq.NArith.Ndigits]
Nshiftr_nat_equiv [lemma, in Coq.NArith.Ndigits]
Nshiftr_nat_S [lemma, in Coq.NArith.Ndigits]
Nsize [abbreviation, in Coq.NArith.Ndigits]
NSqrt [library]
NSqrtProp [module, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.add_sqrt_le [lemma, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.Private_NZSqrt [module, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_add_le [definition, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_succ_or [lemma, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_succ_le [lemma, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_mul_above [lemma, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_mul_below [definition, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_le_lin [lemma, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_lt_lin [definition, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_2 [definition, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_1 [definition, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_0 [definition, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_lt_square [lemma, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_le_square [lemma, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_lt_cancel [definition, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_le_mono [definition, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_square [lemma, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_unique [definition, in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_spec' [lemma, in Coq.Numbers.Natural.Abstract.NSqrt]
Nsqrt_spec [abbreviation, in Coq.NArith.Nsqrt_def]
Nsqrt_def [library]
Nsth [lemma, in Coq.setoid_ring.InitialRing]
NStrongRec [library]
NStrongRecProp [module, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.StrongRecursion [section, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.StrongRecursion.A [variable, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.StrongRecursion.Aeq [variable, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.StrongRecursion.Aeq_equiv [variable, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.StrongRecursion.FixPoint [section, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.StrongRecursion.FixPoint.f [variable, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.StrongRecursion.FixPoint.f_wd [variable, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.StrongRecursion.FixPoint.step_good [variable, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec_any_fst_arg [lemma, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec_0_any [lemma, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec_fixpoint [lemma, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec0_fixpoint [lemma, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec0_more_steps [lemma, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec_0 [lemma, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec0_succ [lemma, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec0_0 [lemma, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec_wd [instance, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec0_wd [instance, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec_alt [lemma, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec0 [definition, in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec [definition, in Coq.Numbers.Natural.Abstract.NStrongRec]
Nsub [definition, in Coq.setoid_ring.InitialRing]
NSub [library]
NSubProp [module, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.add_dichotomy [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.add_sub_swap [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.add_sub_eq_nz [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.add_sub_eq_r [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.add_sub_eq_l [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.add_sub [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.add_sub_assoc [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.le_alt_dichotomy [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.le_alt_wd [instance, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.le_equiv [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.le_alt [definition, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.le_add_le_sub_l [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.le_add_le_sub_r [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.le_sub_le_add_l [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.le_sub_le_add_r [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.le_sub_l [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.lt_alt_wd [instance, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.lt_equiv [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.lt_alt [definition, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.lt_add_lt_sub_l [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.lt_add_lt_sub_r [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.lt_sub_lt_add_l [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.lt_sub_lt_add_r [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.mul_sub_distr_l [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.mul_sub_distr_r [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.mul_pred_r [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_le_mono_l [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_le_mono_r [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_lt [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_add_le [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_0_le [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_add_distr [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_add [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_succ_l [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_gt [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_diag [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_succ [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_0_l [lemma, in Coq.Numbers.Natural.Abstract.NSub]
Nsucc_0 [abbreviation, in Coq.NArith.BinNat]
Ntestbit_Nbit [lemma, in Coq.NArith.Ndigits]
nth [record, in Coq.setoid_ring.Ncring_tac]
nth [definition, in Coq.setoid_ring.BinList]
Nth [lemma, in Coq.setoid_ring.InitialRing]
nth [definition, in Coq.Vectors.VectorDef]
nth [definition, in Coq.micromega.Env]
nth [definition, in Coq.Lists.List]
ntheq_eqst [lemma, in Coq.Lists.Streams]
nth_map2 [lemma, in Coq.Vectors.VectorSpec]
nth_map [lemma, in Coq.Vectors.VectorSpec]
nth_order_last [lemma, in Coq.Vectors.VectorSpec]
nth_le [lemma, in Coq.Arith.Between]
nth_S [constructor, in Coq.Arith.Between]
nth_O [constructor, in Coq.Arith.Between]
nth_pred_double [lemma, in Coq.setoid_ring.BinList]
nth_jump [lemma, in Coq.setoid_ring.BinList]
nth_order [definition, in Coq.Vectors.VectorDef]
nth_pred_double [lemma, in Coq.micromega.Env]
nth_jump [lemma, in Coq.micromega.Env]
nth_spec [lemma, in Coq.micromega.Env]
nth_error_app2 [lemma, in Coq.Lists.List]
nth_error_app1 [lemma, in Coq.Lists.List]
nth_error_split [lemma, in Coq.Lists.List]
nth_error_Some [lemma, in Coq.Lists.List]
nth_error_None [lemma, in Coq.Lists.List]
nth_error_In [lemma, in Coq.Lists.List]
nth_split [lemma, in Coq.Lists.List]
nth_indep [lemma, in Coq.Lists.List]
nth_overflow [lemma, in Coq.Lists.List]
nth_In [lemma, in Coq.Lists.List]
nth_default_eq [lemma, in Coq.Lists.List]
nth_default [definition, in Coq.Lists.List]
nth_error [definition, in Coq.Lists.List]
nth_S_cons [lemma, in Coq.Lists.List]
nth_in_or_default [lemma, in Coq.Lists.List]
nth_ok [definition, in Coq.Lists.List]
NtoZ [definition, in Coq.setoid_ring.Field_theory]
Ntriv_div_th [lemma, in Coq.setoid_ring.InitialRing]
null [inductive, in Coq.btauto.Algebra]
null_intro [constructor, in Coq.btauto.Algebra]
null_derivative_loc [lemma, in Coq.Reals.MVT]
null_derivative_1 [lemma, in Coq.Reals.MVT]
null_derivative_0 [lemma, in Coq.Reals.MVT]
num [projection, in Coq.setoid_ring.Field_theory]
NumPrelude [library]
nuncurry [definition, in Coq.Numbers.NaryFunctions]
nu_left_inv_on [lemma, in Coq.Logic.Eqdep_dec]
Nwadd [definition, in Coq.setoid_ring.InitialRing]
Nwadd_ok [lemma, in Coq.setoid_ring.InitialRing]
Nwcons [definition, in Coq.setoid_ring.InitialRing]
Nweq_bool [definition, in Coq.setoid_ring.InitialRing]
NwI [definition, in Coq.setoid_ring.InitialRing]
Nwmul [definition, in Coq.setoid_ring.InitialRing]
Nwmul_ok [lemma, in Coq.setoid_ring.InitialRing]
NwO [definition, in Coq.setoid_ring.InitialRing]
Nwopp [definition, in Coq.setoid_ring.InitialRing]
Nwopp_ok [lemma, in Coq.setoid_ring.InitialRing]
Nword [definition, in Coq.setoid_ring.InitialRing]
NWORDMORPHISM [section, in Coq.setoid_ring.InitialRing]
NWORDMORPHISM.ARth [variable, in Coq.setoid_ring.InitialRing]
NWORDMORPHISM.R [variable, in Coq.setoid_ring.InitialRing]
NWORDMORPHISM.radd [variable, in Coq.setoid_ring.InitialRing]
NWORDMORPHISM.req [variable, in Coq.setoid_ring.InitialRing]
NWORDMORPHISM.Reqe [variable, in Coq.setoid_ring.InitialRing]
NWORDMORPHISM.rI [variable, in Coq.setoid_ring.InitialRing]
NWORDMORPHISM.rmul [variable, in Coq.setoid_ring.InitialRing]
NWORDMORPHISM.rO [variable, in Coq.setoid_ring.InitialRing]
NWORDMORPHISM.ropp [variable, in Coq.setoid_ring.InitialRing]
NWORDMORPHISM.Rsth [variable, in Coq.setoid_ring.InitialRing]
NWORDMORPHISM.rsub [variable, in Coq.setoid_ring.InitialRing]
_ == _ [notation, in Coq.setoid_ring.InitialRing]
_ - _ [notation, in Coq.setoid_ring.InitialRing]
_ * _ [notation, in Coq.setoid_ring.InitialRing]
_ + _ [notation, in Coq.setoid_ring.InitialRing]
- _ [notation, in Coq.setoid_ring.InitialRing]
0 [notation, in Coq.setoid_ring.InitialRing]
1 [notation, in Coq.setoid_ring.InitialRing]
Nwscal [definition, in Coq.setoid_ring.InitialRing]
Nwscal_ok [lemma, in Coq.setoid_ring.InitialRing]
Nwsub [definition, in Coq.setoid_ring.InitialRing]
Nw_is0 [definition, in Coq.setoid_ring.InitialRing]
Nxor [abbreviation, in Coq.NArith.Ndigits]
Nxor_BVxor [lemma, in Coq.NArith.Ndigits]
Nxor_div2 [lemma, in Coq.NArith.Ndigits]
Nxor_bit0 [lemma, in Coq.NArith.Ndigits]
Nxor_semantics [lemma, in Coq.NArith.Ndigits]
Nxor_nilpotent [abbreviation, in Coq.NArith.Ndigits]
Nxor_neutral_right [abbreviation, in Coq.NArith.Ndigits]
Nxor_neutral_left [abbreviation, in Coq.NArith.Ndigits]
Nxor_assoc [abbreviation, in Coq.NArith.Ndigits]
Nxor_comm [abbreviation, in Coq.NArith.Ndigits]
Nxor_eq [abbreviation, in Coq.NArith.Ndigits]
Nxor_eq_false [lemma, in Coq.NArith.Ndec]
Nxor_eq_true [lemma, in Coq.NArith.Ndec]
NZAdd [library]
NZAddOrder [library]
NZAddOrderProp [module, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_nonneg_cases [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_nonpos_cases [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_pos_cases [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_neg_cases [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_le_cases [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_lt_cases [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_nonneg_nonneg [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_nonneg_pos [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_pos_nonneg [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_pos_pos [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_le_lt_mono [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_lt_le_mono [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_le_mono [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_le_mono_r [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_le_mono_l [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_lt_mono [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_lt_mono_r [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_lt_mono_l [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.le_exists_sub [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.le_le_add_le [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.le_lt_add_lt [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.lt_le_add_lt [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.lt_add_pos_r [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.lt_add_pos_l [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddProp [module, in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_shuffle3 [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_shuffle2 [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_shuffle1 [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_shuffle0 [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_cancel_r [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_cancel_l [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_assoc [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_1_r [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_1_l [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_comm [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_succ_comm [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_succ_r [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_0_r [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddProp.sub_1_r [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAxioms [library]
NZAxiomsSig [module, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig' [module, in Coq.Numbers.NatInt.NZAxioms]
NZBase [library]
NZBaseProp [module, in Coq.Numbers.NatInt.NZBase]
NZBaseProp.CentralInduction [section, in Coq.Numbers.NatInt.NZBase]
NZBaseProp.CentralInduction.A [variable, in Coq.Numbers.NatInt.NZBase]
NZBaseProp.CentralInduction.A_wd [variable, in Coq.Numbers.NatInt.NZBase]
NZBaseProp.central_induction [lemma, in Coq.Numbers.NatInt.NZBase]
NZBaseProp.eq_stepl [lemma, in Coq.Numbers.NatInt.NZBase]
NZBaseProp.eq_sym_iff [lemma, in Coq.Numbers.NatInt.NZBase]
NZBaseProp.neq_sym [lemma, in Coq.Numbers.NatInt.NZBase]
NZBaseProp.succ_inj_wd_neg [lemma, in Coq.Numbers.NatInt.NZBase]
NZBaseProp.succ_inj_wd [lemma, in Coq.Numbers.NatInt.NZBase]
NZBaseProp.succ_inj [lemma, in Coq.Numbers.NatInt.NZBase]
NZBasicFunsSig [module, in Coq.Numbers.NatInt.NZAxioms]
NZBasicFunsSig' [module, in Coq.Numbers.NatInt.NZAxioms]
NZBits [module, in Coq.Numbers.NatInt.NZBits]
NZBits [library]
NZBitsSpec [module, in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.div2_spec [axiom, in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.land_spec [axiom, in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.ldiff_spec [axiom, in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.lor_spec [axiom, in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.lxor_spec [axiom, in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.shiftl_spec_low [axiom, in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.shiftl_spec_high [axiom, in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.shiftr_spec [axiom, in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.testbit_neg_r [axiom, in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.testbit_even_succ [axiom, in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.testbit_odd_succ [axiom, in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.testbit_even_0 [axiom, in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.testbit_odd_0 [axiom, in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.testbit_wd [instance, in Coq.Numbers.NatInt.NZBits]
NZBits' [module, in Coq.Numbers.NatInt.NZBits]
NZCyclic [library]
NZCyclicAxiomsMod [module, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.add [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.add_succ_l [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.add_0_l [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.add_wd [instance, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.bi_induction [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.BS [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.B_holds [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.B0 [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.eq [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.eq_equiv [instance, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.gt_wB_0 [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.gt_wB_1 [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.Induction [section, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.Induction.A [variable, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.Induction.AS [variable, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.Induction.A_wd [variable, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.Induction.A0 [variable, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.Induction.B [variable, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.mul [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.mul_succ_l [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.mul_0_l [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.mul_wd [instance, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZ_to_Z_mod [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.one [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.one_succ [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.one_mod_wB [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.P [abbreviation, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.pred [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.pred_succ [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.pred_mod_wB [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.pred_wd [instance, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.S [abbreviation, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.sub [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.sub_succ_r [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.sub_0_r [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.sub_wd [instance, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.succ [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.succ_mod_wB [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.succ_wd [instance, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.t [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.two [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.two_succ [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.wB [abbreviation, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.Zbounded_induction [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.zero [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
_ * _ [notation, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
_ - _ [notation, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
_ + _ [notation, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
_ == _ [notation, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
0 [notation, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
[| _ |] [notation, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZDecOrdAxiomsSig [module, in Coq.Numbers.NatInt.NZAxioms]
NZDecOrdAxiomsSig' [module, in Coq.Numbers.NatInt.NZAxioms]
NZDecOrdSig [module, in Coq.Numbers.NatInt.NZAxioms]
NZDecOrdSig' [module, in Coq.Numbers.NatInt.NZAxioms]
NZDiv [module, in Coq.Numbers.NatInt.NZDiv]
NZDiv [library]
NZDivProp [module, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.add_mod [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.add_mod_idemp_r [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.add_mod_idemp_l [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_mul_le [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_div [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_mul_cancel_l [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_mul_cancel_r [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_add_l [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_add [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_le_compat_l [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_le_lower_bound [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_le_upper_bound [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_lt_upper_bound [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_exact [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_le_mono [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_lt [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_str_pos_iff [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_small_iff [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_str_pos [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_pos [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_mul [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_1_l [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_1_r [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_0_l [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_small [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_same [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_unique_exact [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_unique [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_mod_unique [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_divides [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_mul_r [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_mod [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_add [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_small_iff [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_le [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_mul [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_1_l [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_1_r [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_0_l [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_small [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_same [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_unique [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mul_mod [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mul_mod_idemp_r [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mul_mod_idemp_l [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mul_mod_distr_r [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mul_mod_distr_l [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mul_succ_div_gt [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mul_div_le [lemma, in Coq.Numbers.NatInt.NZDiv]
NZDivSpec [module, in Coq.Numbers.NatInt.NZDiv]
NZDivSpec.div_mod [axiom, in Coq.Numbers.NatInt.NZDiv]
NZDivSpec.div_wd [instance, in Coq.Numbers.NatInt.NZDiv]
NZDivSpec.mod_bound_pos [axiom, in Coq.Numbers.NatInt.NZDiv]
NZDivSpec.mod_wd [instance, in Coq.Numbers.NatInt.NZDiv]
NZDiv' [module, in Coq.Numbers.NatInt.NZDiv]
NZDomain [library]
NZDomainProp [module, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.bi_induction_pred [lemma, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.central_induction_pred [lemma, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.initial [definition, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.InitialDontExists [section, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.InitialDontExists.succ_onto [variable, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.InitialExists [section, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.InitialExists.init [variable, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.InitialExists.Initial [variable, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.InitialExists.SuccPred [section, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.InitialExists.SuccPred.eq_decidable [variable, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.initial_ancestor [lemma, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.initial_unique [lemma, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.initial_alt2 [lemma, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.initial_alt [lemma, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.itersucc_or_iterpred [lemma, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.itersucc_or_itersucc [lemma, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.itersucc0_or_iterpred0 [lemma, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.succ_onto_pred_injective [lemma, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.succ_onto_gives_succ_pred [lemma, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.succ_pred_approx [lemma, in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.succ_swap_pred [lemma, in Coq.Numbers.NatInt.NZDomain]
NZDomainSig [module, in Coq.Numbers.NatInt.NZAxioms]
NZDomainSig' [module, in Coq.Numbers.NatInt.NZAxioms]
NZGcd [module, in Coq.Numbers.NatInt.NZGcd]
NZGcd [library]
NZGcdProp [module, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_gcd_iff [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_pos_le [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_factor_r [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_factor_l [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_mul_r [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_mul_l [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_add_r [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_antisym_nonneg [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_transitive [instance, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_reflexive [instance, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_trans [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_refl [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_1_r_nonneg [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_0_l [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_0_r [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_1_l [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_wd [instance, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.eq_mul_1_nonneg' [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.eq_mul_1_nonneg [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_mul_diag_l [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_eq_0 [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_eq_0_r [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_eq_0_l [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_diag_nonneg [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_1_r [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_1_l [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_0_r_nonneg [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_0_l_nonneg [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_assoc [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_comm [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_unique_alt [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_divide_iff [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_wd [instance, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_unique [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.mul_divide_cancel_r [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.mul_divide_cancel_l [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.mul_divide_mono_r [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.mul_divide_mono_l [lemma, in Coq.Numbers.NatInt.NZGcd]
NZGcdSpec [module, in Coq.Numbers.NatInt.NZGcd]
NZGcdSpec.divide [definition, in Coq.Numbers.NatInt.NZGcd]
NZGcdSpec.gcd_nonneg [axiom, in Coq.Numbers.NatInt.NZGcd]
NZGcdSpec.gcd_greatest [axiom, in Coq.Numbers.NatInt.NZGcd]
NZGcdSpec.gcd_divide_r [axiom, in Coq.Numbers.NatInt.NZGcd]
NZGcdSpec.gcd_divide_l [axiom, in Coq.Numbers.NatInt.NZGcd]
( _ | _ ) [notation, in Coq.Numbers.NatInt.NZGcd]
NZGcd' [module, in Coq.Numbers.NatInt.NZGcd]
nzhead [definition, in Coq.Init.Decimal]
nzhead_invol [lemma, in Coq.Numbers.DecimalFacts]
nzhead_nonzero [lemma, in Coq.Numbers.DecimalFacts]
nzhead_rev [lemma, in Coq.Numbers.DecimalFacts]
nzhead_revapp [lemma, in Coq.Numbers.DecimalFacts]
nzhead_revapp_0 [lemma, in Coq.Numbers.DecimalFacts]
NZLog [library]
NZLog2 [module, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop [module, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.add_log2_lt [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_add_le [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_succ_double [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_eq_succ_iff_pow2 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_eq_succ_is_pow2 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_succ_or [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_succ_le [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_same [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_double [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_mul_pow2 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_mul_above [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_mul_below [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_le_lin [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_lt_lin [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_lt_pow2 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_le_pow2 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_lt_cancel [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_le_mono [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_null [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_pos [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_2 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_1 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_pred_pow2 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_pow2 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_unique' [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_spec_alt [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_wd [instance, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_unique [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_nonneg [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2Spec [module, in Coq.Numbers.NatInt.NZLog]
NZLog2Spec.log2_nonpos [axiom, in Coq.Numbers.NatInt.NZLog]
NZLog2Spec.log2_spec [axiom, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp [module, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.add_log2_up_lt [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.le_log2_up_succ_log2 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.le_log2_log2_up [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_add_le [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_succ_double [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_eq_succ_iff_pow2 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_eq_succ_is_pow2 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_succ_or [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_succ_le [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_same [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_double [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_mul_pow2 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_mul_below [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_mul_above [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_le_lin [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_lt_lin [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_le_pow2 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_lt_pow2 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_lt_cancel [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_le_mono [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_null [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_pos [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_log2_up_exact [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_log2_up_spec [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_2 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_1 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_succ_pow2 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_pow2 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_unique [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_nonneg [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_wd [instance, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_nonpos [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_spec [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_eqn [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_eqn0 [lemma, in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up [definition, in Coq.Numbers.NatInt.NZLog]
NZMul [library]
NZMulOrder [library]
NZMulOrderProp [module, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.add_square_le [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.add_le_mul [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.crossmul_le_addsquare [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.eq_mul_0_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.eq_mul_0_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.eq_square_0 [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.eq_mul_0 [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.lt_0_mul [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.lt_1_mul_pos [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_2_mono_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_eq_0_r [definition, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_eq_0_l [definition, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_eq_0 [definition, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_nonneg_cancel_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_nonneg_cancel_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_pos_cancel_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_pos_cancel_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_nonneg_nonneg [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_neg_pos [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_pos_neg [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_neg_neg [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_pos_pos [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_le_mono_nonneg [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_lt_mono_nonneg [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_le_mono_neg_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_le_mono_neg_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_le_mono_pos_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_le_mono_pos_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_id_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_id_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_cancel_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_cancel_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_le_mono_nonpos_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_le_mono_nonneg_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_le_mono_nonpos_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_le_mono_nonneg_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_lt_mono_neg_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_lt_mono_neg_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_lt_mono_pos_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_lt_mono_pos_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_lt_pred [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.neq_mul_0 [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.quadmul_le_squareadd [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.square_add_le [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.square_nonneg [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.square_le_simpl_nonneg [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.square_lt_simpl_nonneg [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.square_le_mono_nonneg [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.square_lt_mono_nonneg [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulProp [module, in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_shuffle3 [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_shuffle2 [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_shuffle1 [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_shuffle0 [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_1_r [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_1_l [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_assoc [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_add_distr_l [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_add_distr_r [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_comm [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_succ_r [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_0_r [lemma, in Coq.Numbers.NatInt.NZMul]
NZOfNat [module, in Coq.Numbers.NatInt.NZDomain]
NZOfNatOps [module, in Coq.Numbers.NatInt.NZDomain]
NZOfNatOps.ofnat_sub [lemma, in Coq.Numbers.NatInt.NZDomain]
NZOfNatOps.ofnat_sub_r [lemma, in Coq.Numbers.NatInt.NZDomain]
NZOfNatOps.ofnat_mul [lemma, in Coq.Numbers.NatInt.NZDomain]
NZOfNatOps.ofnat_add [lemma, in Coq.Numbers.NatInt.NZDomain]
NZOfNatOps.ofnat_add_l [lemma, in Coq.Numbers.NatInt.NZDomain]
NZOfNatOrd [module, in Coq.Numbers.NatInt.NZDomain]
NZOfNatOrd.ofnat_le [lemma, in Coq.Numbers.NatInt.NZDomain]
NZOfNatOrd.ofnat_lt [lemma, in Coq.Numbers.NatInt.NZDomain]
NZOfNatOrd.ofnat_eq [lemma, in Coq.Numbers.NatInt.NZDomain]
NZOfNatOrd.ofnat_injective [lemma, in Coq.Numbers.NatInt.NZDomain]
NZOfNatOrd.ofnat_S_neq_0 [lemma, in Coq.Numbers.NatInt.NZDomain]
NZOfNatOrd.ofnat_S_gt_0 [lemma, in Coq.Numbers.NatInt.NZDomain]
NZOfNat.ofnat [definition, in Coq.Numbers.NatInt.NZDomain]
NZOfNat.ofnat_pred [lemma, in Coq.Numbers.NatInt.NZDomain]
NZOfNat.ofnat_succ [lemma, in Coq.Numbers.NatInt.NZDomain]
NZOfNat.ofnat_zero [lemma, in Coq.Numbers.NatInt.NZDomain]
[ _ ] (ofnat) [notation, in Coq.Numbers.NatInt.NZDomain]
NZOrd [module, in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig [module, in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig' [module, in Coq.Numbers.NatInt.NZAxioms]
NZOrder [library]
NZOrderProp [module, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.A'A_left [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.A'A_right [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.eq_dne [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.eq_decidable [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.eq_le_incl [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.gt_wf [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Induction [section, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Induction.A [variable, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Induction.A_wd [variable, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Induction.Center [section, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Induction.Center.LeftInduction [section, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Induction.Center.LeftInduction.A' [variable, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Induction.Center.LeftInduction.left_step'' [variable, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Induction.Center.LeftInduction.left_step' [variable, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Induction.Center.LeftInduction.left_step [variable, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Induction.Center.RightInduction [section, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Induction.Center.RightInduction.A' [variable, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Induction.Center.RightInduction.right_step'' [variable, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Induction.Center.RightInduction.right_step' [variable, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Induction.Center.RightInduction.right_step [variable, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Induction.Center.z [variable, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lbase [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.left_induction' [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.left_induction [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_ind [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_dne [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_decidable [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_ngt [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_ge_cases [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_0_2 [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_0_1 [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_le_succ_r [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_succ_r [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_antisymm [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_lt_trans [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_stepr [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_stepl [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_neq [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_lteq [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_partialorder [instance, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_preorder [instance, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_trans [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_gt_cases [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_succ_l [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_succ_diag_r [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_refl [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_wd [instance, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.ls_ls' [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.ls'_ls'' [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_wf [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_ind [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_succ_pred [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_exists_pred [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_exists_pred_strong [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_nge [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_dne [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_decidable [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_gt_cases [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_ge_cases [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_1_l [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_0_2 [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_1_2 [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_0_1 [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_lt_succ_r [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_succ_l [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_le_trans [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_stepr [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_stepl [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_neq [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_total [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_compat [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_strorder [instance, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_trans [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_ngt [abbreviation, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_asymm [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_eq_gt_cases [abbreviation, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_trichotomy [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_succ_diag_r [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_le_incl [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.neq_succ_diag_r [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.neq_succ_diag_l [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.nle_gt [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.nle_succ_diag_l [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.nlt_succ_r [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.nlt_ge [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.nlt_succ_diag_l [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.order_induction'_0 [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.order_induction_0 [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.order_induction' [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.order_induction [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Private_OrderTac.Tac [module, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Private_OrderTac.IsTotal.le_lteq [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Private_OrderTac.IsTotal.lt_total [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Private_OrderTac.IsTotal.lt_compat [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Private_OrderTac.IsTotal.lt_strorder [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Private_OrderTac.IsTotal.eq_equiv [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Private_OrderTac.IsTotal [module, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Private_OrderTac [module, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.rbase [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Rgt_wd [instance, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.right_induction' [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.right_induction [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.Rlt_wd [instance, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.rs_rs' [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.rs'_rs'' [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.strong_left_induction' [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.strong_left_induction [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.strong_right_induction' [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.strong_right_induction [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.succ_le_mono [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.succ_lt_mono [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.WF [section, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.WF.Rgt [variable, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.WF.Rlt [variable, in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.WF.z [variable, in Coq.Numbers.NatInt.NZOrder]
NZOrdSig [module, in Coq.Numbers.NatInt.NZAxioms]
NZOrdSig' [module, in Coq.Numbers.NatInt.NZAxioms]
NZOrd' [module, in Coq.Numbers.NatInt.NZAxioms]
Nzorn [lemma, in Coq.Reals.RiemannInt_SF]
NZParity [module, in Coq.Numbers.NatInt.NZParity]
NZParity [library]
NZParityProp [module, in Coq.Numbers.NatInt.NZParity]
NZParityProp.double_above [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.double_below [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_add_mul_2 [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_add_mul_even [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_add_even [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_mul [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_add [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_succ_succ [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.Even_succ_succ [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.Even_succ [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_succ [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_2 [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_1 [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_0 [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.Even_Odd_False [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.Even_or_Odd [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_wd [instance, in Coq.Numbers.NatInt.NZParity]
NZParityProp.Even_wd [instance, in Coq.Numbers.NatInt.NZParity]
NZParityProp.negb_even [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.negb_odd [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_add_mul_2 [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_add_mul_even [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_add_even [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_mul [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_add [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_succ_succ [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.Odd_succ_succ [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_succ [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.Odd_succ [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_2 [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_1 [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_0 [lemma, in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_wd [instance, in Coq.Numbers.NatInt.NZParity]
NZParityProp.Odd_wd [instance, in Coq.Numbers.NatInt.NZParity]
NZParityProp.orb_even_odd [lemma, in Coq.Numbers.NatInt.NZParity]
NZParity.Even [definition, in Coq.Numbers.NatInt.NZParity]
NZParity.even [axiom, in Coq.Numbers.NatInt.NZParity]
NZParity.even_spec [axiom, in Coq.Numbers.NatInt.NZParity]
NZParity.Odd [definition, in Coq.Numbers.NatInt.NZParity]
NZParity.odd [axiom, in Coq.Numbers.NatInt.NZParity]
NZParity.odd_spec [axiom, in Coq.Numbers.NatInt.NZParity]
NZPow [module, in Coq.Numbers.NatInt.NZPow]
NZPow [library]
NZPowProp [module, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_add_upper [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_add_lower [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_gt_lin_r [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_le_mono_r_iff [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_lt_mono_r_iff [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_le_mono_l_iff [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_lt_mono_l_iff [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_inj_r [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_inj_l [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_lt_mono [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_le_mono [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_le_mono_r [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_lt_mono_r [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_gt_1 [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_le_mono_l [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_lt_mono_l [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_pos_nonneg [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_nonneg [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_mul_r [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_mul_l [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_add_r [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_eq_0_iff [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_nonzero [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_eq_0 [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_2_r [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_1_l [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_1_r [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_0_l' [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_0_l [lemma, in Coq.Numbers.NatInt.NZPow]
NZPowSpec [module, in Coq.Numbers.NatInt.NZPow]
NZPowSpec.pow_neg_r [axiom, in Coq.Numbers.NatInt.NZPow]
NZPowSpec.pow_succ_r [axiom, in Coq.Numbers.NatInt.NZPow]
NZPowSpec.pow_0_r [axiom, in Coq.Numbers.NatInt.NZPow]
NZPowSpec.pow_wd [instance, in Coq.Numbers.NatInt.NZPow]
NZPow' [module, in Coq.Numbers.NatInt.NZPow]
NZProp [module, in Coq.Numbers.NatInt.NZProperties]
NZProperties [library]
NZSqrt [module, in Coq.Numbers.NatInt.NZSqrt]
NZSqrt [library]
NZSqrtProp [module, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.add_sqrt_le [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_add_le [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_eq_succ_iff_square [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_succ_or [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_succ_le [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_mul_above [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_mul_below [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_le_lin [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_lt_lin [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_pos [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_2 [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_1 [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_0 [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_lt_square [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_le_square [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_lt_cancel [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_le_mono [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_pred_square [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_square [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_unique' [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_spec_alt [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_wd [instance, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_unique [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_nonneg [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_spec_nonneg [lemma, in Coq.Numbers.NatInt.NZSqrt]
_ ² [notation, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtSpec [module, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtSpec.sqrt_neg [axiom, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtSpec.sqrt_spec [axiom, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp [module, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.add_sqrt_up_le [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.le_sqrt_up_succ_sqrt [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.le_sqrt_sqrt_up [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_add_le [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_eq_succ_iff_square [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_succ_or [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_succ_le [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_mul_below [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_mul_above [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_le_lin [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_lt_lin [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_pos [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_le_square [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_lt_square [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_lt_cancel [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_le_mono [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_sqrt_up_exact [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_sqrt_up_spec [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_2 [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_1 [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_0 [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_succ_square [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_square [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_unique [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_wd [instance, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_nonneg [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_spec [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_eqn [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_eqn0 [lemma, in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up [definition, in Coq.Numbers.NatInt.NZSqrt]
_ ² [notation, in Coq.Numbers.NatInt.NZSqrt]
√° _ [notation, in Coq.Numbers.NatInt.NZSqrt]
NZSqrt' [module, in Coq.Numbers.NatInt.NZSqrt]
NZSquare [module, in Coq.Numbers.NatInt.NZAxioms]
NZSquare.square [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZSquare.square_spec [axiom, in Coq.Numbers.NatInt.NZAxioms]
nztail [definition, in Coq.Init.Decimal]
nztail [definition, in Coq.Numbers.DecimalFacts]
nztail_int [definition, in Coq.Init.Decimal]
N_digits [definition, in Coq.ZArith.Zlogarithm]
N_of_max [abbreviation, in Coq.NArith.Nnat]
N_of_min [abbreviation, in Coq.NArith.Nnat]
N_of_nat_compare [abbreviation, in Coq.NArith.Nnat]
N_of_div2 [abbreviation, in Coq.NArith.Nnat]
N_of_mult [abbreviation, in Coq.NArith.Nnat]
N_of_minus [abbreviation, in Coq.NArith.Nnat]
N_of_plus [abbreviation, in Coq.NArith.Nnat]
N_of_pred [abbreviation, in Coq.NArith.Nnat]
N_of_S [abbreviation, in Coq.NArith.Nnat]
N_of_double_plus_one [abbreviation, in Coq.NArith.Nnat]
N_of_double [abbreviation, in Coq.NArith.Nnat]
N_of_nat_inj [abbreviation, in Coq.NArith.Nnat]
N_of_nat_of_N [abbreviation, in Coq.NArith.Nnat]
N_as_DT [module, in Coq.Structures.DecidableTypeEx]
N_nat_Z [lemma, in Coq.ZArith.Znat]
N_of_Z [abbreviation, in Coq.setoid_ring.ZArithRing]
N_ascii_bounded [lemma, in Coq.Strings.Ascii]
N_ascii_embedding [lemma, in Coq.Strings.Ascii]
N_of_ascii [definition, in Coq.Strings.Ascii]
N_of_digits [definition, in Coq.Strings.Ascii]
N_as_DT [module, in Coq.Structures.OrdersEx]
N_as_OT [module, in Coq.Structures.OrdersEx]
n_SSSSn [lemma, in Coq.Arith.Plus]
n_SSSn [lemma, in Coq.Arith.Plus]
n_SSn [lemma, in Coq.Arith.Plus]
n_of_int [definition, in Coq.extraction.ExtrOcamlIntConv]
n_Sn [lemma, in Coq.Init.Peano]
N_rec_double [definition, in Coq.NArith.BinNat]
N_ind_double [definition, in Coq.NArith.BinNat]
N_of_nat [abbreviation, in Coq.NArith.BinNat]
N_ind [abbreviation, in Coq.NArith.BinNat]
N_rec [abbreviation, in Coq.NArith.BinNat]
N_rect [abbreviation, in Coq.NArith.BinNat]
n_of_Z [abbreviation, in Coq.micromega.ZMicromega]
n_to_z [definition, in Coq.Numbers.AltBinNotations]
n_of_z [definition, in Coq.Numbers.AltBinNotations]
N_as_OT.eq_dec [definition, in Coq.Structures.OrderedTypeEx]
N_as_OT.compare [definition, in Coq.Structures.OrderedTypeEx]
N_as_OT.lt_not_eq [definition, in Coq.Structures.OrderedTypeEx]
N_as_OT.lt_trans [definition, in Coq.Structures.OrderedTypeEx]
N_as_OT.lt [definition, in Coq.Structures.OrderedTypeEx]
N_as_OT.eq_trans [definition, in Coq.Structures.OrderedTypeEx]
N_as_OT.eq_sym [definition, in Coq.Structures.OrderedTypeEx]
N_as_OT.eq_refl [definition, in Coq.Structures.OrderedTypeEx]
N_as_OT.eq [definition, in Coq.Structures.OrderedTypeEx]
N_as_OT.t [definition, in Coq.Structures.OrderedTypeEx]
N_as_OT [module, in Coq.Structures.OrderedTypeEx]
n_of_bigint [definition, in Coq.extraction.ExtrOcamlBigIntConv]
N.add [definition, in Coq.NArith.BinNatDef]
N.add_succ_l [lemma, in Coq.NArith.BinNat]
N.add_0_l [lemma, in Coq.NArith.BinNat]
N.add_wd [definition, in Coq.NArith.BinNat]
N.binary_ind [definition, in Coq.NArith.BinNat]
N.binary_rec [definition, in Coq.NArith.BinNat]
N.binary_rect [definition, in Coq.NArith.BinNat]
N.bi_induction [lemma, in Coq.NArith.BinNat]
N.compare [definition, in Coq.NArith.BinNatDef]
N.compare_0_r [lemma, in Coq.NArith.BinNat]
N.compare_antisym [lemma, in Coq.NArith.BinNat]
N.compare_le_iff [lemma, in Coq.NArith.BinNat]
N.compare_lt_iff [lemma, in Coq.NArith.BinNat]
N.compare_eq_iff [lemma, in Coq.NArith.BinNat]
N.discr [definition, in Coq.NArith.BinNat]
N.div [definition, in Coq.NArith.BinNatDef]
N.divide [definition, in Coq.NArith.BinNat]
N.div_eucl [definition, in Coq.NArith.BinNatDef]
N.div_mod [definition, in Coq.NArith.BinNat]
N.div_mod' [lemma, in Coq.NArith.BinNat]
N.div_eucl_spec [lemma, in Coq.NArith.BinNat]
N.div_wd [definition, in Coq.NArith.BinNat]
N.div2 [definition, in Coq.NArith.BinNatDef]
N.div2_spec [definition, in Coq.NArith.BinNat]
N.div2_succ_double [lemma, in Coq.NArith.BinNat]
N.div2_double [lemma, in Coq.NArith.BinNat]
N.double [definition, in Coq.NArith.BinNatDef]
N.double_le_mono [lemma, in Coq.NArith.BinNat]
N.double_lt_mono [lemma, in Coq.NArith.BinNat]
N.double_inj [lemma, in Coq.NArith.BinNat]
N.double_mul [lemma, in Coq.NArith.BinNat]
N.double_add [lemma, in Coq.NArith.BinNat]
N.double_spec [lemma, in Coq.NArith.BinNat]
N.eq [definition, in Coq.NArith.BinNat]
N.eqb [definition, in Coq.NArith.BinNatDef]
N.eqb_eq [lemma, in Coq.NArith.BinNat]
N.eq_dec [definition, in Coq.NArith.BinNat]
N.eq_equiv [definition, in Coq.NArith.BinNat]
N.even [definition, in Coq.NArith.BinNatDef]
N.Even [definition, in Coq.NArith.BinNat]
N.even_spec [lemma, in Coq.NArith.BinNat]
N.gcd [definition, in Coq.NArith.BinNatDef]
N.gcd_nonneg [lemma, in Coq.NArith.BinNat]
N.gcd_greatest [lemma, in Coq.NArith.BinNat]
N.gcd_divide_r [lemma, in Coq.NArith.BinNat]
N.gcd_divide_l [lemma, in Coq.NArith.BinNat]
N.ge [definition, in Coq.NArith.BinNat]
N.ge_le [lemma, in Coq.NArith.BinNat]
N.ge_le_iff [lemma, in Coq.NArith.BinNat]
N.ggcd [definition, in Coq.NArith.BinNatDef]
N.ggcd_correct_divisors [lemma, in Coq.NArith.BinNat]
N.ggcd_gcd [lemma, in Coq.NArith.BinNat]
N.gt [definition, in Coq.NArith.BinNat]
N.gt_lt [lemma, in Coq.NArith.BinNat]
N.gt_lt_iff [lemma, in Coq.NArith.BinNat]
N.iter [definition, in Coq.NArith.BinNatDef]
N.land [definition, in Coq.NArith.BinNatDef]
N.land_spec [lemma, in Coq.NArith.BinNat]
N.ldiff [definition, in Coq.NArith.BinNatDef]
N.ldiff_spec [lemma, in Coq.NArith.BinNat]
N.le [definition, in Coq.NArith.BinNat]
N.leb [definition, in Coq.NArith.BinNatDef]
N.leb_le [lemma, in Coq.NArith.BinNat]
N.le_ge [lemma, in Coq.NArith.BinNat]
N.log2 [definition, in Coq.NArith.BinNatDef]
N.log2_nonpos [lemma, in Coq.NArith.BinNat]
N.log2_spec [lemma, in Coq.NArith.BinNat]
N.lor [definition, in Coq.NArith.BinNatDef]
N.lor_spec [lemma, in Coq.NArith.BinNat]
N.lt [definition, in Coq.NArith.BinNat]
N.ltb [definition, in Coq.NArith.BinNatDef]
N.ltb_lt [lemma, in Coq.NArith.BinNat]
N.lt_gt [lemma, in Coq.NArith.BinNat]
N.lt_succ_r [lemma, in Coq.NArith.BinNat]
N.lt_wd [definition, in Coq.NArith.BinNat]
N.lxor [definition, in Coq.NArith.BinNatDef]
N.lxor_spec [lemma, in Coq.NArith.BinNat]
N.max [definition, in Coq.NArith.BinNatDef]
N.max_r [lemma, in Coq.NArith.BinNat]
N.max_l [lemma, in Coq.NArith.BinNat]
N.min [definition, in Coq.NArith.BinNatDef]
N.min_r [lemma, in Coq.NArith.BinNat]
N.min_l [lemma, in Coq.NArith.BinNat]
N.modulo [definition, in Coq.NArith.BinNatDef]
N.mod_bound_pos [lemma, in Coq.NArith.BinNat]
N.mod_lt [lemma, in Coq.NArith.BinNat]
N.mod_wd [definition, in Coq.NArith.BinNat]
N.mul [definition, in Coq.NArith.BinNatDef]
N.mul_succ_l [lemma, in Coq.NArith.BinNat]
N.mul_0_l [lemma, in Coq.NArith.BinNat]
N.mul_wd [definition, in Coq.NArith.BinNat]
N.odd [definition, in Coq.NArith.BinNatDef]
N.Odd [definition, in Coq.NArith.BinNat]
N.odd_spec [lemma, in Coq.NArith.BinNat]
N.of_int [definition, in Coq.NArith.BinNatDef]
N.of_uint [definition, in Coq.NArith.BinNatDef]
N.of_nat [definition, in Coq.NArith.BinNatDef]
N.one [definition, in Coq.NArith.BinNatDef]
N.one_succ [lemma, in Coq.NArith.BinNat]
N.peano_rec_succ [lemma, in Coq.NArith.BinNat]
N.peano_rec_base [lemma, in Coq.NArith.BinNat]
N.peano_rec [definition, in Coq.NArith.BinNat]
N.peano_ind [definition, in Coq.NArith.BinNat]
N.peano_rect_succ [lemma, in Coq.NArith.BinNat]
N.peano_rect_base [lemma, in Coq.NArith.BinNat]
N.peano_rect [definition, in Coq.NArith.BinNat]
N.pos [abbreviation, in Coq.NArith.BinNatDef]
N.pos_div_eucl [definition, in Coq.NArith.BinNatDef]
N.pos_pred_shiftl_high [lemma, in Coq.NArith.BinNat]
N.pos_pred_shiftl_low [lemma, in Coq.NArith.BinNat]
N.pos_ldiff_spec [lemma, in Coq.NArith.BinNat]
N.pos_land_spec [lemma, in Coq.NArith.BinNat]
N.pos_lor_spec [lemma, in Coq.NArith.BinNat]
N.pos_lxor_spec [lemma, in Coq.NArith.BinNat]
N.pos_div_eucl_remainder [lemma, in Coq.NArith.BinNat]
N.pos_div_eucl_spec [lemma, in Coq.NArith.BinNat]
N.pos_pred_succ [lemma, in Coq.NArith.BinNat]
N.pos_pred_spec [lemma, in Coq.NArith.BinNat]
N.pow [definition, in Coq.NArith.BinNatDef]
N.pow_neg_r [lemma, in Coq.NArith.BinNat]
N.pow_succ_r [lemma, in Coq.NArith.BinNat]
N.pow_0_r [lemma, in Coq.NArith.BinNat]
N.pow_wd [definition, in Coq.NArith.BinNat]
N.pred [definition, in Coq.NArith.BinNatDef]
N.pred_div2_up [lemma, in Coq.NArith.BinNat]
N.pred_sub [lemma, in Coq.NArith.BinNat]
N.pred_succ [lemma, in Coq.NArith.BinNat]
N.pred_0 [definition, in Coq.NArith.BinNat]
N.pred_wd [definition, in Coq.NArith.BinNat]
N.recursion [definition, in Coq.NArith.BinNat]
N.recursion_succ [lemma, in Coq.NArith.BinNat]
N.recursion_0 [lemma, in Coq.NArith.BinNat]
N.recursion_wd [instance, in Coq.NArith.BinNat]
N.shiftl [definition, in Coq.NArith.BinNatDef]
N.shiftl_nat [definition, in Coq.NArith.BinNatDef]
N.shiftl_spec_low [lemma, in Coq.NArith.BinNat]
N.shiftl_spec_high [lemma, in Coq.NArith.BinNat]
N.shiftl_succ_r [lemma, in Coq.NArith.BinNat]
N.shiftr [definition, in Coq.NArith.BinNatDef]
N.shiftr_nat [definition, in Coq.NArith.BinNatDef]
N.shiftr_spec [lemma, in Coq.NArith.BinNat]
N.shiftr_succ_r [lemma, in Coq.NArith.BinNat]
N.size [definition, in Coq.NArith.BinNatDef]
N.size_nat [definition, in Coq.NArith.BinNatDef]
N.size_le [lemma, in Coq.NArith.BinNat]
N.size_gt [lemma, in Coq.NArith.BinNat]
N.size_log2 [lemma, in Coq.NArith.BinNat]
N.sqrt [definition, in Coq.NArith.BinNatDef]
N.sqrtrem [definition, in Coq.NArith.BinNatDef]
N.sqrtrem_spec [lemma, in Coq.NArith.BinNat]
N.sqrtrem_sqrt [lemma, in Coq.NArith.BinNat]
N.sqrt_neg [lemma, in Coq.NArith.BinNat]
N.sqrt_spec [lemma, in Coq.NArith.BinNat]
N.square [definition, in Coq.NArith.BinNatDef]
N.square_spec [lemma, in Coq.NArith.BinNat]
N.sub [definition, in Coq.NArith.BinNatDef]
N.sub_succ_r [lemma, in Coq.NArith.BinNat]
N.sub_0_r [lemma, in Coq.NArith.BinNat]
N.sub_wd [definition, in Coq.NArith.BinNat]
N.succ [definition, in Coq.NArith.BinNatDef]
N.succ_pos [definition, in Coq.NArith.BinNatDef]
N.succ_double [definition, in Coq.NArith.BinNatDef]
N.succ_double_le_mono [lemma, in Coq.NArith.BinNat]
N.succ_double_lt_mono [lemma, in Coq.NArith.BinNat]
N.succ_double_lt [lemma, in Coq.NArith.BinNat]
N.succ_double_inj [lemma, in Coq.NArith.BinNat]
N.succ_double_mul [lemma, in Coq.NArith.BinNat]
N.succ_double_add [lemma, in Coq.NArith.BinNat]
N.succ_double_spec [lemma, in Coq.NArith.BinNat]
N.succ_0_discr [lemma, in Coq.NArith.BinNat]
N.succ_pos_pred [lemma, in Coq.NArith.BinNat]
N.succ_pos_spec [lemma, in Coq.NArith.BinNat]
N.succ_wd [definition, in Coq.NArith.BinNat]
N.t [definition, in Coq.NArith.BinNatDef]
N.testbit [definition, in Coq.NArith.BinNatDef]
N.testbit_nat [definition, in Coq.NArith.BinNatDef]
N.testbit_neg_r [lemma, in Coq.NArith.BinNat]
N.testbit_even_succ [lemma, in Coq.NArith.BinNat]
N.testbit_odd_succ [lemma, in Coq.NArith.BinNat]
N.testbit_succ_r_div2 [lemma, in Coq.NArith.BinNat]
N.testbit_odd_0 [lemma, in Coq.NArith.BinNat]
N.testbit_even_0 [lemma, in Coq.NArith.BinNat]
N.testbit_wd [definition, in Coq.NArith.BinNat]
N.to_int [definition, in Coq.NArith.BinNatDef]
N.to_uint [definition, in Coq.NArith.BinNatDef]
N.to_nat [definition, in Coq.NArith.BinNatDef]
N.two [definition, in Coq.NArith.BinNatDef]
N.two_succ [lemma, in Coq.NArith.BinNat]
N.zero [definition, in Coq.NArith.BinNatDef]
_ mod _ (N_scope) [notation, in Coq.NArith.BinNatDef]
_ / _ (N_scope) [notation, in Coq.NArith.BinNatDef]
_ ^ _ (N_scope) [notation, in Coq.NArith.BinNatDef]
_ [notation, in Coq.NArith.BinNatDef]
_ <=? _ (N_scope) [notation, in Coq.NArith.BinNatDef]
_ =? _ (N_scope) [notation, in Coq.NArith.BinNatDef]
_ ?= _ (N_scope) [notation, in Coq.NArith.BinNatDef]
_ * _ (N_scope) [notation, in Coq.NArith.BinNatDef]
_ - _ (N_scope) [notation, in Coq.NArith.BinNatDef]
_ + _ (N_scope) [notation, in Coq.NArith.BinNatDef]
( _ | _ ) (N_scope) [notation, in Coq.NArith.BinNat]
_ < _ <= _ (N_scope) [notation, in Coq.NArith.BinNat]
_ < _ < _ (N_scope) [notation, in Coq.NArith.BinNat]
_ <= _ < _ (N_scope) [notation, in Coq.NArith.BinNat]
_ <= _ <= _ (N_scope) [notation, in Coq.NArith.BinNat]
_ > _ (N_scope) [notation, in Coq.NArith.BinNat]
_ >= _ (N_scope) [notation, in Coq.NArith.BinNat]
_ < _ (N_scope) [notation, in Coq.NArith.BinNat]
_ <= _ (N_scope) [notation, in Coq.NArith.BinNat]
N0 [abbreviation, in Coq.NArith.BinNat]
N0 [constructor, in Coq.Numbers.BinNums]
N0_less_2 [lemma, in Coq.NArith.Ndigits]
N0_less_1 [lemma, in Coq.NArith.Ndigits]
N2Bv [definition, in Coq.NArith.Ndigits]
N2Bv_N2Bv_sized_above [lemma, in Coq.NArith.Ndigits]
N2Bv_sized_Bv2N [lemma, in Coq.NArith.Ndigits]
N2Bv_sized_Nsize [lemma, in Coq.NArith.Ndigits]
N2Bv_Bv2N [lemma, in Coq.NArith.Ndigits]
N2Bv_N2Bv_gen_above [lemma, in Coq.NArith.Ndigits]
N2Bv_N2Bv_gen [lemma, in Coq.NArith.Ndigits]
N2Bv_gen [definition, in Coq.NArith.Ndigits]
N2Bv_sized [definition, in Coq.NArith.Ndigits]
N2ByteV_sized [definition, in Coq.NArith.Ndigits]
N2Nat [module, in Coq.NArith.Nnat]
N2Nat.id [lemma, in Coq.NArith.Nnat]
N2Nat.inj [lemma, in Coq.NArith.Nnat]
N2Nat.inj_iter [lemma, in Coq.NArith.Nnat]
N2Nat.inj_min [lemma, in Coq.NArith.Nnat]
N2Nat.inj_max [lemma, in Coq.NArith.Nnat]
N2Nat.inj_compare [lemma, in Coq.NArith.Nnat]
N2Nat.inj_div2 [lemma, in Coq.NArith.Nnat]
N2Nat.inj_pred [lemma, in Coq.NArith.Nnat]
N2Nat.inj_sub [lemma, in Coq.NArith.Nnat]
N2Nat.inj_mul [lemma, in Coq.NArith.Nnat]
N2Nat.inj_add [lemma, in Coq.NArith.Nnat]
N2Nat.inj_succ [lemma, in Coq.NArith.Nnat]
N2Nat.inj_succ_double [lemma, in Coq.NArith.Nnat]
N2Nat.inj_double [lemma, in Coq.NArith.Nnat]
N2Nat.inj_iff [lemma, in Coq.NArith.Nnat]
N2Z [module, in Coq.ZArith.Znat]
N2Z.id [lemma, in Coq.ZArith.Znat]
N2Z.inj [lemma, in Coq.ZArith.Znat]
N2Z.inj_testbit [lemma, in Coq.ZArith.Znat]
N2Z.inj_pow [lemma, in Coq.ZArith.Znat]
N2Z.inj_quot2 [lemma, in Coq.ZArith.Znat]
N2Z.inj_div2 [lemma, in Coq.ZArith.Znat]
N2Z.inj_rem [lemma, in Coq.ZArith.Znat]
N2Z.inj_quot [lemma, in Coq.ZArith.Znat]
N2Z.inj_mod [lemma, in Coq.ZArith.Znat]
N2Z.inj_div [lemma, in Coq.ZArith.Znat]
N2Z.inj_max [lemma, in Coq.ZArith.Znat]
N2Z.inj_min [lemma, in Coq.ZArith.Znat]
N2Z.inj_pred [lemma, in Coq.ZArith.Znat]
N2Z.inj_pred_max [lemma, in Coq.ZArith.Znat]
N2Z.inj_succ [lemma, in Coq.ZArith.Znat]
N2Z.inj_sub [lemma, in Coq.ZArith.Znat]
N2Z.inj_sub_max [lemma, in Coq.ZArith.Znat]
N2Z.inj_mul [lemma, in Coq.ZArith.Znat]
N2Z.inj_add [lemma, in Coq.ZArith.Znat]
N2Z.inj_abs_N [lemma, in Coq.ZArith.Znat]
N2Z.inj_gt [lemma, in Coq.ZArith.Znat]
N2Z.inj_ge [lemma, in Coq.ZArith.Znat]
N2Z.inj_lt [lemma, in Coq.ZArith.Znat]
N2Z.inj_le [lemma, in Coq.ZArith.Znat]
N2Z.inj_compare [lemma, in Coq.ZArith.Znat]
N2Z.inj_pos [lemma, in Coq.ZArith.Znat]
N2Z.inj_0 [lemma, in Coq.ZArith.Znat]
N2Z.inj_iff [lemma, in Coq.ZArith.Znat]
N2Z.is_nonneg [lemma, in Coq.ZArith.Znat]
| 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 | (22221 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 | (923 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 | (744 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 | (1480 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 | (501 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 | (10364 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 | (910 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 | (573 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 | (386 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 | (286 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 | (465 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 | (632 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 | (1133 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 | (3679 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 | (145 entries) |