| 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 | (25958 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 | (999 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 | (811 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 | (1769 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 | (587 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 | (11879 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 | (960 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (508 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (307 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (479 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (495 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 | (905 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 | (1199 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 | (4894 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (166 entries) |
N (lemma)
NAddOrderProp.add_pos_r [in Coq.Numbers.Natural.Abstract.NAddOrder]NAddOrderProp.add_pos_l [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderProp.le_add_l [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderProp.le_add_r [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderProp.lt_lt_add_l [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderProp.lt_lt_add_r [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddProp.add_pred_r [in Coq.Numbers.Natural.Abstract.NAdd]
NAddProp.add_pred_l [in Coq.Numbers.Natural.Abstract.NAdd]
NAddProp.eq_add_1 [in Coq.Numbers.Natural.Abstract.NAdd]
NAddProp.eq_add_succ [in Coq.Numbers.Natural.Abstract.NAdd]
NAddProp.eq_add_0 [in Coq.Numbers.Natural.Abstract.NAdd]
NAddProp.succ_add_discr [in Coq.Numbers.Natural.Abstract.NAdd]
nandP [in Coq.ssr.ssrbool]
narrow_interval_lower_bound [in Coq.micromega.ZMicromega]
nary_congruence [in Coq.ssr.ssreflect]
Nath [in Coq.setoid_ring.InitialRing]
natlike_rec3 [in Coq.ZArith.Wf_Z]
natlike_rec2 [in Coq.ZArith.Wf_Z]
natlike_rec [in Coq.ZArith.Wf_Z]
natlike_ind [in Coq.ZArith.Wf_Z]
NatOfZ [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
NatOrder.leb_total [in Coq.Sorting.Mergesort]
natSRth [in Coq.setoid_ring.ArithRing]
nat_rect_plus [in Coq.Init.Peano]
nat_rect_succ_r [in Coq.Init.Peano]
nat_double_ind [in Coq.Init.Peano]
nat_case [in Coq.Init.Peano]
nat_of_P_lt_Lt_compare_complement_morphism [in Coq.PArith.Pnat]
nat_of_P_gt_Gt_compare_morphism [in Coq.PArith.Pnat]
nat_of_P_lt_Lt_compare_morphism [in Coq.PArith.Pnat]
nat_of_P_minus_morphism [in Coq.PArith.Pnat]
nat_compare_equiv [in Coq.Arith.Compare_dec]
nat_compare_Gt_gt [in Coq.Arith.Compare_dec]
nat_compare_Lt_lt [in Coq.Arith.Compare_dec]
nat_compare_eq [in Coq.Arith.Compare_dec]
nat_compare_ge [in Coq.Arith.Compare_dec]
nat_compare_le [in Coq.Arith.Compare_dec]
nat_compare_gt [in Coq.Arith.Compare_dec]
nat_compare_lt [in Coq.Arith.Compare_dec]
nat_morph_N [in Coq.setoid_ring.ArithRing]
nat_bijection_Permutation [in Coq.Sorting.Permutation]
Nat_as_OT.lt_not_eq [in Coq.Structures.OrderedTypeEx]
Nat_as_OT.lt_trans [in Coq.Structures.OrderedTypeEx]
nat_ascii_bounded [in Coq.Strings.Ascii]
nat_ascii_embedding [in Coq.Strings.Ascii]
nat_N_Z [in Coq.ZArith.Znat]
Nat.add_succ_l [in Coq.Arith.PeanoNat]
Nat.add_0_l [in Coq.Arith.PeanoNat]
Nat.binary_induction [in Coq.Arith.PeanoNat]
Nat.bi_induction [in Coq.Arith.PeanoNat]
Nat.compare_succ [in Coq.Arith.PeanoNat]
Nat.compare_antisym [in Coq.Arith.PeanoNat]
Nat.compare_le_iff [in Coq.Arith.PeanoNat]
Nat.compare_lt_iff [in Coq.Arith.PeanoNat]
Nat.compare_eq_iff [in Coq.Arith.PeanoNat]
Nat.divmod_spec [in Coq.Arith.PeanoNat]
Nat.div_0_r [in Coq.Arith.PeanoNat]
Nat.div_mod [in Coq.Arith.PeanoNat]
Nat.div_mod_eq [in Coq.Arith.PeanoNat]
Nat.double_twice [in Coq.Arith.PeanoNat]
Nat.eqb_eq [in Coq.Arith.PeanoNat]
Nat.eq_dec [in Coq.Arith.PeanoNat]
Nat.EvenT_OddT_rect [in Coq.Arith.PeanoNat]
Nat.EvenT_OddT_dec [in Coq.Arith.PeanoNat]
Nat.EvenT_even [in Coq.Arith.PeanoNat]
Nat.EvenT_Even [in Coq.Arith.PeanoNat]
Nat.EvenT_S_OddT [in Coq.Arith.PeanoNat]
Nat.EvenT_2 [in Coq.Arith.PeanoNat]
Nat.EvenT_0 [in Coq.Arith.PeanoNat]
Nat.Even_EvenT [in Coq.Arith.PeanoNat]
Nat.even_EvenT [in Coq.Arith.PeanoNat]
Nat.Even_Odd_sind [in Coq.Arith.PeanoNat]
Nat.Even_Odd_ind [in Coq.Arith.PeanoNat]
Nat.even_spec [in Coq.Arith.PeanoNat]
Nat.gcd_nonneg [in Coq.Arith.PeanoNat]
Nat.gcd_greatest [in Coq.Arith.PeanoNat]
Nat.gcd_divide_r [in Coq.Arith.PeanoNat]
Nat.gcd_divide_l [in Coq.Arith.PeanoNat]
Nat.gcd_divide [in Coq.Arith.PeanoNat]
Nat.iter_invariant [in Coq.Arith.PeanoNat]
Nat.iter_rect [in Coq.Arith.PeanoNat]
Nat.iter_ind [in Coq.Arith.PeanoNat]
Nat.iter_add [in Coq.Arith.PeanoNat]
Nat.iter_succ_r [in Coq.Arith.PeanoNat]
Nat.iter_succ [in Coq.Arith.PeanoNat]
Nat.iter_swap [in Coq.Arith.PeanoNat]
Nat.iter_swap_gen [in Coq.Arith.PeanoNat]
Nat.leb_le [in Coq.Arith.PeanoNat]
Nat.log2_nonpos [in Coq.Arith.PeanoNat]
Nat.log2_spec [in Coq.Arith.PeanoNat]
Nat.log2_iter_spec [in Coq.Arith.PeanoNat]
Nat.ltb_lt [in Coq.Arith.PeanoNat]
Nat.lt_succ_r [in Coq.Arith.PeanoNat]
Nat.max_r [in Coq.Arith.PeanoNat]
Nat.max_l [in Coq.Arith.PeanoNat]
Nat.min_r [in Coq.Arith.PeanoNat]
Nat.min_l [in Coq.Arith.PeanoNat]
Nat.mod_0_r [in Coq.Arith.PeanoNat]
Nat.mod_bound_pos [in Coq.Arith.PeanoNat]
Nat.mul_succ_l [in Coq.Arith.PeanoNat]
Nat.mul_0_l [in Coq.Arith.PeanoNat]
Nat.OddT_EvenT_rect [in Coq.Arith.PeanoNat]
Nat.OddT_odd [in Coq.Arith.PeanoNat]
Nat.OddT_Odd [in Coq.Arith.PeanoNat]
Nat.OddT_S_EvenT [in Coq.Arith.PeanoNat]
Nat.OddT_2 [in Coq.Arith.PeanoNat]
Nat.OddT_1 [in Coq.Arith.PeanoNat]
Nat.Odd_OddT [in Coq.Arith.PeanoNat]
Nat.odd_OddT [in Coq.Arith.PeanoNat]
Nat.Odd_Even_sind [in Coq.Arith.PeanoNat]
Nat.Odd_Even_ind [in Coq.Arith.PeanoNat]
Nat.odd_spec [in Coq.Arith.PeanoNat]
Nat.one_succ [in Coq.Arith.PeanoNat]
Nat.pow_succ_r [in Coq.Arith.PeanoNat]
Nat.pow_0_r [in Coq.Arith.PeanoNat]
Nat.pow_neg_r [in Coq.Arith.PeanoNat]
Nat.pred_0 [in Coq.Arith.PeanoNat]
Nat.pred_succ [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.div2_spec [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.div2_bitwise [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.div2_decr [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.div2_succ_double [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.div2_double [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.land_spec [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.ldiff_spec [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.le_div2 [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.lor_spec [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.lt_div2 [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.lxor_spec [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.odd_bitwise [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.shiftl_spec_low [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.shiftl_specif_high [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.shiftr_specif [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.testbit_neg_r [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.testbit_bitwise_2 [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.testbit_bitwise_1 [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.testbit_even_succ' [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.testbit_odd_succ' [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.testbit_even_0 [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.testbit_odd_0 [in Coq.Arith.PeanoNat]
Nat.PrivateImplementsBitwiseSpec.testbit_0_l [in Coq.Arith.PeanoNat]
Nat.Private_Parity.Odd_2 [in Coq.Arith.PeanoNat]
Nat.Private_Parity.Odd_1 [in Coq.Arith.PeanoNat]
Nat.Private_Parity.Odd_0 [in Coq.Arith.PeanoNat]
Nat.Private_Parity.Even_2 [in Coq.Arith.PeanoNat]
Nat.Private_Parity.Even_1 [in Coq.Arith.PeanoNat]
Nat.Private_Parity.Even_0 [in Coq.Arith.PeanoNat]
Nat.recursion_succ [in Coq.Arith.PeanoNat]
Nat.recursion_0 [in Coq.Arith.PeanoNat]
Nat.sqrt_neg [in Coq.Arith.PeanoNat]
Nat.sqrt_specif [in Coq.Arith.PeanoNat]
Nat.sqrt_iter_spec [in Coq.Arith.PeanoNat]
Nat.square_spec [in Coq.Arith.PeanoNat]
Nat.strong_induction_le [in Coq.Arith.PeanoNat]
Nat.sub_succ_r [in Coq.Arith.PeanoNat]
Nat.sub_0_r [in Coq.Arith.PeanoNat]
Nat.tail_mul_spec [in Coq.Arith.PeanoNat]
Nat.tail_addmul_spec [in Coq.Arith.PeanoNat]
Nat.tail_add_spec [in Coq.Arith.PeanoNat]
Nat.two_succ [in Coq.Arith.PeanoNat]
Nat2N.id [in Coq.NArith.Nnat]
Nat2N.inj [in Coq.NArith.Nnat]
Nat2N.inj_iter [in Coq.NArith.Nnat]
Nat2N.inj_max [in Coq.NArith.Nnat]
Nat2N.inj_min [in Coq.NArith.Nnat]
Nat2N.inj_pow [in Coq.NArith.Nnat]
Nat2N.inj_mod [in Coq.NArith.Nnat]
Nat2N.inj_div [in Coq.NArith.Nnat]
Nat2N.inj_compare [in Coq.NArith.Nnat]
Nat2N.inj_div2 [in Coq.NArith.Nnat]
Nat2N.inj_mul [in Coq.NArith.Nnat]
Nat2N.inj_sub [in Coq.NArith.Nnat]
Nat2N.inj_add [in Coq.NArith.Nnat]
Nat2N.inj_pred [in Coq.NArith.Nnat]
Nat2N.inj_succ [in Coq.NArith.Nnat]
Nat2N.inj_succ_double [in Coq.NArith.Nnat]
Nat2N.inj_double [in Coq.NArith.Nnat]
Nat2N.inj_iff [in Coq.NArith.Nnat]
Nat2Pos.id [in Coq.PArith.Pnat]
Nat2Pos.id_max [in Coq.PArith.Pnat]
Nat2Pos.inj [in Coq.PArith.Pnat]
Nat2Pos.inj_pow [in Coq.PArith.Pnat]
Nat2Pos.inj_max [in Coq.PArith.Pnat]
Nat2Pos.inj_min [in Coq.PArith.Pnat]
Nat2Pos.inj_sub [in Coq.PArith.Pnat]
Nat2Pos.inj_compare [in Coq.PArith.Pnat]
Nat2Pos.inj_mul [in Coq.PArith.Pnat]
Nat2Pos.inj_add [in Coq.PArith.Pnat]
Nat2Pos.inj_pred [in Coq.PArith.Pnat]
Nat2Pos.inj_succ [in Coq.PArith.Pnat]
Nat2Pos.inj_0 [in Coq.PArith.Pnat]
Nat2Pos.inj_iff [in Coq.PArith.Pnat]
Nat2Z.id [in Coq.ZArith.Znat]
Nat2Z.inj [in Coq.ZArith.Znat]
Nat2Z.inj_double [in Coq.ZArith.Znat]
Nat2Z.inj_div2 [in Coq.ZArith.Znat]
Nat2Z.inj_pow [in Coq.ZArith.Znat]
Nat2Z.inj_mod [in Coq.ZArith.Znat]
Nat2Z.inj_div [in Coq.ZArith.Znat]
Nat2Z.inj_max [in Coq.ZArith.Znat]
Nat2Z.inj_min [in Coq.ZArith.Znat]
Nat2Z.inj_pred [in Coq.ZArith.Znat]
Nat2Z.inj_pred_max [in Coq.ZArith.Znat]
Nat2Z.inj_sub [in Coq.ZArith.Znat]
Nat2Z.inj_sub_max [in Coq.ZArith.Znat]
Nat2Z.inj_mul [in Coq.ZArith.Znat]
Nat2Z.inj_add [in Coq.ZArith.Znat]
Nat2Z.inj_abs_nat [in Coq.ZArith.Znat]
Nat2Z.inj_gt [in Coq.ZArith.Znat]
Nat2Z.inj_ge [in Coq.ZArith.Znat]
Nat2Z.inj_lt [in Coq.ZArith.Znat]
Nat2Z.inj_le [in Coq.ZArith.Znat]
Nat2Z.inj_compare [in Coq.ZArith.Znat]
Nat2Z.inj_iff [in Coq.ZArith.Znat]
Nat2Z.inj_succ [in Coq.ZArith.Znat]
Nat2Z.inj_0 [in Coq.ZArith.Znat]
Nat2Z.is_nonneg [in Coq.ZArith.Znat]
NBaseProp.case_analysis [in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.double_induction [in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.eq_pred_0 [in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.induction [in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.le_0_l [in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.neq_0_r [in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.neq_0 [in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.neq_0_succ [in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.neq_succ_0 [in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.pair_induction [in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.pred_inj [in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.succ_pred [in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.two_dim_induction [in Coq.Numbers.Natural.Abstract.NBase]
NBaseProp.zero_or_succ [in Coq.Numbers.Natural.Abstract.NBase]
NBitsProp.add_nocarry_mod_lt_pow2 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_nocarry_lt_pow2 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_lnot_diag_low [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_nocarry_lxor [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_bit1 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_carry_bits [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_carry_div2 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_bit0 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_b2n_double_bit0 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add_b2n_double_div2 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add3_bits_div2 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.add3_bit0 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.are_bits [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.bits_inj_iff [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.bits_inj [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.bits_inj_0 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.bits_above_log2 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.bits_0 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.bit_log2 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.bit0_mod [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.bit0_eqb [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.bit0_odd [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.b2n_bit0 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.b2n_div2 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.b2n_inj [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.b2n_le_1 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.clearbit_neq [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.clearbit_eq [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.clearbit_iff [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.clearbit_eqb [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.clearbit_spec' [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.div_pow2_bits [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.div2_decr [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.div2_le_lower_bound [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.div2_le_upper_bound [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.div2_odd' [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.div2_even [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.div2_odd [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.div2_le_mono [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.div2_1 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.div2_0 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.div2_div [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.div2_bits [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.double_bits_succ [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.exists_div2 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_lnot_diag_low [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_lnot_diag [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_ones_low [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_ones [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_ldiff [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_lor_distr_r [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_lor_distr_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_le_r [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_le_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_odd_odd [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_even_odd [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_odd_even [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_even_even [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_odd_r [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_odd_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_even_r [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_even_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_diag [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_assoc [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_comm [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_0_r [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.land_0_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_le [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_land_low [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_ones_l_low [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_ones_r_low [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_ones_r [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_ldiff_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_le_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_odd_odd [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_even_odd [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_odd_even [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_even_even [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_odd_r [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_even_r [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_odd_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_even_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_diag [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_0_r [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ldiff_0_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.le_div2 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.le_div2_diag_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_sub_low [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_lxor_r [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_lxor_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_ldiff_low [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_land_low [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_lor_low [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_ones [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_0_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_involutive [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_spec_high [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lnot_spec_low [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.log2_lxor [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.log2_land [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.log2_lor [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.log2_shiftl [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.log2_shiftr [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.log2_bits_unique [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_lnot_diag_low [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_lnot_diag [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_ones_low [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_ldiff_and [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_land_distr_r [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_land_distr_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_eq_0_iff [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_eq_0_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_diag [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_assoc [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_comm [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_0_r [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lor_0_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lt_div2 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lt_div2_diag_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_lor [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_lnot_lnot [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_assoc [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_comm [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_0_r [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_0_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_eq_0_iff [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_nilpotent [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor_eq [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.mod_pow2_bits_low [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.mod_pow2_bits_high [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.mul_pow2_bits_low [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.mul_pow2_bits_high [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.mul_pow2_bits_add [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.nocarry_equiv [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ones_succ [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ones_spec_iff [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ones_spec_high [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ones_spec_low [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ones_mod_pow2 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ones_div_pow2 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ones_add [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ones_0 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.ones_equiv [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.pow_div_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.pow_sub_r [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.pow2_bits_eqb [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.pow2_bits_false [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.pow2_bits_true [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.Private_binary_induction [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.setbit_neq [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.setbit_eq [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.setbit_iff [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.setbit_eqb [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.setbit_spec' [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_lower_bound [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_ldiff [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_lor [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_land [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_lxor [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_eq_0_iff [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_0_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_0_r [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_1_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_shiftl [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_spec_alt [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_mul_pow2 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftl_spec_high' [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_upper_bound [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_ldiff [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_lor [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_land [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_lxor [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_eq_0 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_eq_0_iff [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_0_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_0_r [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_shiftl_r [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_shiftl_l [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_shiftr [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_div_pow2 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.shiftr_spec' [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.sub_nocarry_ldiff [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_div2 [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_odd [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_unique [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_eqb [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_false [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_true [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_spec [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_spec' [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_even_succ' [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_odd_succ' [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_succ_r [in Coq.Numbers.Natural.Abstract.NBits]
NBitsProp.testbit_0_r [in Coq.Numbers.Natural.Abstract.NBits]
Nbit0_neq [in Coq.NArith.Ndec]
nb_digits_del_head_sub [in Coq.Numbers.DecimalFacts]
nb_digits_rev [in Coq.Numbers.DecimalFacts]
nb_digits_unorm [in Coq.Numbers.DecimalFacts]
nb_digits_nzhead [in Coq.Numbers.DecimalFacts]
nb_digits_iter_D0 [in Coq.Numbers.DecimalFacts]
nb_digits_n0 [in Coq.Numbers.DecimalFacts]
nb_digits_0 [in Coq.Numbers.DecimalFacts]
nb_digits_spec [in Coq.Numbers.DecimalFacts]
nb_digits_del_head_sub [in Coq.Numbers.HexadecimalFacts]
nb_digits_rev [in Coq.Numbers.HexadecimalFacts]
nb_digits_unorm [in Coq.Numbers.HexadecimalFacts]
nb_digits_nzhead [in Coq.Numbers.HexadecimalFacts]
nb_digits_iter_D0 [in Coq.Numbers.HexadecimalFacts]
nb_digits_n0 [in Coq.Numbers.HexadecimalFacts]
nb_digits_0 [in Coq.Numbers.HexadecimalFacts]
nb_digits_spec [in Coq.Numbers.HexadecimalFacts]
Ncompare_antisym [in Coq.NArith.BinNat]
Ncompare_Lt_Nltb [in Coq.NArith.Ndec]
Ncompare_Gt_Nltb [in Coq.NArith.Ndec]
Ncompare_Neqb [in Coq.NArith.Ndec]
NdefOpsProp.def_mul_mul [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.def_mul_succ_r [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.def_mul_0_r [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.def_add_add [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.def_add_succ_l [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.def_add_0_l [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.even_succ [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.even_0 [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_decrease [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_nz [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_lower_bound [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_upper_bound [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_double [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_1 [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_0 [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_aux_spec2 [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_aux_spec [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_aux_succ [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.half_aux_0 [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.if_zero_succ [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.if_zero_0 [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.log_step [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.log_init [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.log_good_step [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.ltb_ge [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.ltb_lt [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.ltb_0_succ [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.ltb_0 [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.ltb_step [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.ltb_base [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.pow_succ [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.pow_0 [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.pow2_log [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsProp.succ_ltb_mono [in Coq.Numbers.Natural.Abstract.NDefOps]
NDivProp.add_mul_mod_distr_r [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.add_mul_mod_distr_l [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.add_mod [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.add_mod_idemp_r [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.add_mod_idemp_l [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_mul_le [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_div [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_mul_cancel_l [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_mul_cancel_r [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_add_l [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_add [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_le_compat_l [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_le_lower_bound [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_le_upper_bound [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_lt_upper_bound [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_exact [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_le_mono [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_lt [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_str_pos_iff [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_small_iff [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_str_pos [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_mul [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_1_l [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_1_r [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_0_l [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_small [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_same [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_unique_exact [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_unique [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.div_mod_unique [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_divides [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_mul_r [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_mod [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_add [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_small_iff [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_le [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_mul [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_1_l [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_1_r [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_0_l [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_small [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_same [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_unique [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_eq [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mod_upper_bound [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mul_mod [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mul_mod_idemp_r [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mul_mod_idemp_l [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mul_mod_distr_l [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mul_mod_distr_r [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mul_succ_div_gt [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp.mul_div_le [in Coq.Numbers.Natural.Abstract.NDiv]
NDivProp0.Div0.add_mul_mod_distr_r [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.add_mul_mod_distr_l [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.add_mod [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.add_mod_idemp_r [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.add_mod_idemp_l [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.div_mul_le [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.div_div [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.div_mul_cancel_l [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.div_mul_cancel_r [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.div_le_upper_bound [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.div_lt_upper_bound [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.div_exact [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.div_le_mono [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.div_mod [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.div_0_l [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.mod_divides [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.mod_mul_r [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.mod_mod [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.mod_add [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.mod_le [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.mod_mul [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.mod_same [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.mod_eq [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.mod_0_l [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.mul_mod [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.mul_mod_idemp_r [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.mul_mod_idemp_l [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.mul_mod_distr_l [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.mul_mod_distr_r [in Coq.Numbers.Natural.Abstract.NDiv0]
NDivProp0.Div0.mul_div_le [in Coq.Numbers.Natural.Abstract.NDiv0]
Ndiv2_bit_neq [in Coq.NArith.Ndec]
Ndiv2_bit_eq [in Coq.NArith.Ndec]
Ndiv2_neq [in Coq.NArith.Ndec]
Ndiv2_eq [in Coq.NArith.Ndec]
Ndouble_or_double_plus_un [in Coq.NArith.Ndec]
negate_correct [in Coq.micromega.RingMicromega]
negate_correct [in Coq.micromega.ZMicromega]
negative_derivative [in Coq.Reals.MVT]
negbF [in Coq.ssr.ssrbool]
negbFE [in Coq.ssr.ssrbool]
negbK [in Coq.ssr.ssrbool]
negbLR [in Coq.ssr.ssrbool]
negbNE [in Coq.ssr.ssrbool]
negbRL [in Coq.ssr.ssrbool]
negbT [in Coq.ssr.ssrbool]
negbTE [in Coq.ssr.ssrbool]
negb_imply [in Coq.ssr.ssrbool]
negb_or [in Coq.ssr.ssrbool]
negb_and [in Coq.ssr.ssrbool]
negb_inj [in Coq.ssr.ssrbool]
negb_if [in Coq.Bool.Bool]
negb_prop_involutive [in Coq.Bool.Bool]
negb_prop_classical [in Coq.Bool.Bool]
negb_prop_intro [in Coq.Bool.Bool]
negb_prop_elim [in Coq.Bool.Bool]
negb_xorb_r [in Coq.Bool.Bool]
negb_xorb_l [in Coq.Bool.Bool]
negb_xorb [in Coq.Bool.Bool]
negb_false_iff [in Coq.Bool.Bool]
negb_true_iff [in Coq.Bool.Bool]
negb_sym [in Coq.Bool.Bool]
negb_involutive_reverse [in Coq.Bool.Bool]
negb_involutive [in Coq.Bool.Bool]
negb_andb [in Coq.Bool.Bool]
negb_orb [in Coq.Bool.Bool]
negP [in Coq.ssr.ssrbool]
negPartAbsMin [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
negPf [in Coq.ssr.ssrbool]
negPn [in Coq.ssr.ssrbool]
negPP [in Coq.ssr.ssrbool]
neg_sin [in Coq.Reals.Rtrigo1]
neg_cos [in Coq.Reals.Rtrigo1]
neg_Forall_Exists_neg [in Coq.Lists.List]
neg_false [in Coq.Init.Logic]
neg_pos_Rsqr_lt [in Coq.Reals.R_sqr]
neg_pos_Rsqr_le [in Coq.Reals.R_sqr]
neighbourhood_P1 [in Coq.Reals.Rtopology]
Neqb_ok [in Coq.setoid_ring.InitialRing]
Neqb_complete [in Coq.NArith.Ndec]
Neqb_Ncompare [in Coq.NArith.Ndec]
Neqe [in Coq.setoid_ring.InitialRing]
nequiv_equiv_trans [in Coq.Classes.SetoidClass]
Neven_not_double_plus_one [in Coq.NArith.Ndec]
Newman [in Coq.Sets.Relations_3_facts]
NewtonInt_P9 [in Coq.Reals.NewtonInt]
NewtonInt_P8 [in Coq.Reals.NewtonInt]
NewtonInt_P7 [in Coq.Reals.NewtonInt]
NewtonInt_P6 [in Coq.Reals.NewtonInt]
NewtonInt_P5 [in Coq.Reals.NewtonInt]
NewtonInt_P4 [in Coq.Reals.NewtonInt]
NewtonInt_P3 [in Coq.Reals.NewtonInt]
NewtonInt_P2 [in Coq.Reals.NewtonInt]
NewtonInt_P1 [in Coq.Reals.NewtonInt]
new_var [in Coq.omega.OmegaLemmas]
nformula_plus_nformula_correct [in Coq.micromega.RingMicromega]
nformula_times_nformula_correct [in Coq.micromega.RingMicromega]
NGcdProp.bezout_comm [in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.bezout_1_gcd [in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_mul_split [in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_sub_r [in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_add_cancel_r [in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gauss [in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_mul_mono_r [in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_mul_mono_l [in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_bezout [in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_bezout_pos_pos [in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_bezout_pos [in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_sub_diag_r [in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_add_diag_r [in Coq.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_add_mult_diag_r [in Coq.Numbers.Natural.Abstract.NGcd]
NilEmpty.isi [in Coq.Numbers.DecimalString]
NilEmpty.isi [in Coq.Numbers.HexadecimalString]
NilEmpty.sis [in Coq.Numbers.DecimalString]
NilEmpty.sis [in Coq.Numbers.HexadecimalString]
NilEmpty.sus [in Coq.Numbers.DecimalString]
NilEmpty.sus [in Coq.Numbers.HexadecimalString]
NilEmpty.usu [in Coq.Numbers.DecimalString]
NilEmpty.usu [in Coq.Numbers.HexadecimalString]
NilZero.isi [in Coq.Numbers.DecimalString]
NilZero.isi [in Coq.Numbers.HexadecimalString]
NilZero.isi_negnil [in Coq.Numbers.DecimalString]
NilZero.isi_posnil [in Coq.Numbers.DecimalString]
NilZero.isi_negnil [in Coq.Numbers.HexadecimalString]
NilZero.isi_posnil [in Coq.Numbers.HexadecimalString]
NilZero.sis [in Coq.Numbers.DecimalString]
NilZero.sis [in Coq.Numbers.HexadecimalString]
NilZero.sus [in Coq.Numbers.DecimalString]
NilZero.sus [in Coq.Numbers.HexadecimalString]
NilZero.uint_of_string_nonnil [in Coq.Numbers.DecimalString]
NilZero.uint_of_string_nonnil [in Coq.Numbers.HexadecimalString]
NilZero.usu [in Coq.Numbers.DecimalString]
NilZero.usu [in Coq.Numbers.HexadecimalString]
NilZero.usu_gen [in Coq.Numbers.DecimalString]
NilZero.usu_nil [in Coq.Numbers.DecimalString]
NilZero.usu_gen [in Coq.Numbers.HexadecimalString]
NilZero.usu_nil [in Coq.Numbers.HexadecimalString]
nil_spec [in Coq.Vectors.VectorSpec]
nil_cons [in Coq.Lists.List]
NLcmProp.divide_lcm_iff [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.divide_lcm_eq_r [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.divide_div [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.divide_lcm_r [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.divide_lcm_l [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.divide_div_mul_exact [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.gcd_1_lcm_mul [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.gcd_div_swap [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.gcd_mod [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.gcd_div_gcd [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.gcd_div_factor [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_mul_mono_r [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_mul_mono_l [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_eq_0 [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_diag [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_1_r [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_1_l [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_0_r [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_0_l [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_assoc [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_unique_alt [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_unique [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_divide_iff [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_comm [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_least [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_equiv2 [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.lcm_equiv1 [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp.mod_divide [in Coq.Numbers.Natural.Abstract.NLcm]
NLcmProp0.Lcm0.divide_div [in Coq.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.Lcm0.divide_div_mul_exact [in Coq.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.Lcm0.gcd_mod [in Coq.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.Lcm0.gcd_div_factor [in Coq.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.Lcm0.lcm_unique_alt [in Coq.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.Lcm0.lcm_unique [in Coq.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.Lcm0.lcm_equiv2 [in Coq.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.Lcm0.lcm_equiv1 [in Coq.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.Lcm0.mod_divide [in Coq.Numbers.Natural.Abstract.NLcm0]
Nleb_double_plus_one_mono_conv [in Coq.NArith.Ndec]
Nleb_double_mono_conv [in Coq.NArith.Ndec]
Nleb_double_plus_one_mono [in Coq.NArith.Ndec]
Nleb_double_mono [in Coq.NArith.Ndec]
Nleb_ltb_trans [in Coq.NArith.Ndec]
Nleb_trans [in Coq.NArith.Ndec]
Nleb_antisym [in Coq.NArith.Ndec]
Nleb_refl [in Coq.NArith.Ndec]
Nleb_Nle [in Coq.NArith.Ndec]
Nleb_alt [in Coq.NArith.Ndec]
Nltb_Ncompare [in Coq.NArith.Ndec]
Nltb_double_plus_one_mono_conv [in Coq.NArith.Ndec]
Nltb_double_mono_conv [in Coq.NArith.Ndec]
Nltb_double_plus_one_mono [in Coq.NArith.Ndec]
Nltb_double_mono [in Coq.NArith.Ndec]
Nltb_leb_weak [in Coq.NArith.Ndec]
Nltb_trans [in Coq.NArith.Ndec]
Nltb_leb_trans [in Coq.NArith.Ndec]
NMaxMinProp.add_min_distr_r [in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.add_min_distr_l [in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.add_max_distr_r [in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.add_max_distr_l [in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.max_0_r [in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.max_0_l [in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.min_0_r [in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.min_0_l [in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.mul_min_distr_r [in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.mul_min_distr_l [in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.mul_max_distr_r [in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.mul_max_distr_l [in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.sub_min_distr_r [in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.sub_min_distr_l [in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.sub_max_distr_r [in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.sub_max_distr_l [in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.succ_min_distr [in Coq.Numbers.Natural.Abstract.NMaxMin]
NMaxMinProp.succ_max_distr [in Coq.Numbers.Natural.Abstract.NMaxMin]
Nmin_lt_4 [in Coq.NArith.Ndec]
Nmin_lt_3 [in Coq.NArith.Ndec]
Nmin_le_5 [in Coq.NArith.Ndec]
Nmin_le_4 [in Coq.NArith.Ndec]
Nmin_le_3 [in Coq.NArith.Ndec]
Nmin_le_2 [in Coq.NArith.Ndec]
Nmin_le_1 [in Coq.NArith.Ndec]
NMulOrderProp.eq_mul_1 [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.le_mul_r [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.le_mul_l [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.lt_0_mul' [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.mul_le_mono [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.mul_lt_mono [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.mul_le_mono_r [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.mul_le_mono_l [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.square_le_mono [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderProp.square_lt_mono [in Coq.Numbers.Natural.Abstract.NMulOrder]
Nmult_reg_r [in Coq.NArith.BinNat]
Nmult_plus_distr_l [in Coq.NArith.BinNat]
Nmult_Sn_m [in Coq.NArith.BinNat]
Nneq_elim [in Coq.NArith.Ndec]
Nnot_div2_not_double_plus_one [in Coq.NArith.Ndec]
Nnot_div2_not_double [in Coq.NArith.Ndec]
NNPP [in Coq.Logic.Classical_Prop]
Nodd_not_double [in Coq.NArith.Ndec]
NodepOfDep.add_3 [in Coq.FSets.FSetBridge]
NodepOfDep.add_2 [in Coq.FSets.FSetBridge]
NodepOfDep.add_1 [in Coq.FSets.FSetBridge]
NodepOfDep.cardinal_1 [in Coq.FSets.FSetBridge]
NodepOfDep.choose_3 [in Coq.FSets.FSetBridge]
NodepOfDep.choose_2 [in Coq.FSets.FSetBridge]
NodepOfDep.choose_1 [in Coq.FSets.FSetBridge]
NodepOfDep.compat_P_aux [in Coq.FSets.FSetBridge]
NodepOfDep.diff_3 [in Coq.FSets.FSetBridge]
NodepOfDep.diff_2 [in Coq.FSets.FSetBridge]
NodepOfDep.diff_1 [in Coq.FSets.FSetBridge]
NodepOfDep.elements_3w [in Coq.FSets.FSetBridge]
NodepOfDep.elements_3 [in Coq.FSets.FSetBridge]
NodepOfDep.elements_2 [in Coq.FSets.FSetBridge]
NodepOfDep.elements_1 [in Coq.FSets.FSetBridge]
NodepOfDep.empty_1 [in Coq.FSets.FSetBridge]
NodepOfDep.equal_2 [in Coq.FSets.FSetBridge]
NodepOfDep.equal_1 [in Coq.FSets.FSetBridge]
NodepOfDep.exists_2 [in Coq.FSets.FSetBridge]
NodepOfDep.exists_1 [in Coq.FSets.FSetBridge]
NodepOfDep.filter_3 [in Coq.FSets.FSetBridge]
NodepOfDep.filter_2 [in Coq.FSets.FSetBridge]
NodepOfDep.filter_1 [in Coq.FSets.FSetBridge]
NodepOfDep.fold_1 [in Coq.FSets.FSetBridge]
NodepOfDep.for_all_2 [in Coq.FSets.FSetBridge]
NodepOfDep.for_all_1 [in Coq.FSets.FSetBridge]
NodepOfDep.inter_3 [in Coq.FSets.FSetBridge]
NodepOfDep.inter_2 [in Coq.FSets.FSetBridge]
NodepOfDep.inter_1 [in Coq.FSets.FSetBridge]
NodepOfDep.is_empty_2 [in Coq.FSets.FSetBridge]
NodepOfDep.is_empty_1 [in Coq.FSets.FSetBridge]
NodepOfDep.max_elt_3 [in Coq.FSets.FSetBridge]
NodepOfDep.max_elt_2 [in Coq.FSets.FSetBridge]
NodepOfDep.max_elt_1 [in Coq.FSets.FSetBridge]
NodepOfDep.mem_2 [in Coq.FSets.FSetBridge]
NodepOfDep.mem_1 [in Coq.FSets.FSetBridge]
NodepOfDep.min_elt_3 [in Coq.FSets.FSetBridge]
NodepOfDep.min_elt_2 [in Coq.FSets.FSetBridge]
NodepOfDep.min_elt_1 [in Coq.FSets.FSetBridge]
NodepOfDep.partition_2 [in Coq.FSets.FSetBridge]
NodepOfDep.partition_1 [in Coq.FSets.FSetBridge]
NodepOfDep.remove_3 [in Coq.FSets.FSetBridge]
NodepOfDep.remove_2 [in Coq.FSets.FSetBridge]
NodepOfDep.remove_1 [in Coq.FSets.FSetBridge]
NodepOfDep.singleton_2 [in Coq.FSets.FSetBridge]
NodepOfDep.singleton_1 [in Coq.FSets.FSetBridge]
NodepOfDep.subset_2 [in Coq.FSets.FSetBridge]
NodepOfDep.subset_1 [in Coq.FSets.FSetBridge]
NodepOfDep.union_3 [in Coq.FSets.FSetBridge]
NodepOfDep.union_2 [in Coq.FSets.FSetBridge]
NodepOfDep.union_1 [in Coq.FSets.FSetBridge]
NoDupA_equivlistA_permut [in Coq.Sorting.PermutSetoid]
NoDupA_equivlistA_decompose [in Coq.Lists.SetoidPermutation]
NoDupA_equivlistA_PermutationA [in Coq.Lists.SetoidPermutation]
NoDupA_singleton [in Coq.Lists.SetoidList]
NoDupA_swap [in Coq.Lists.SetoidList]
NoDupA_split [in Coq.Lists.SetoidList]
NoDupA_rev [in Coq.Lists.SetoidList]
NoDupA_app [in Coq.Lists.SetoidList]
NoDupA_altdef [in Coq.Lists.SetoidList]
NoDup_permut [in Coq.Sorting.PermutEq]
NoDup_concat [in Coq.Lists.List]
NoDup_map_NoDup_ForallPairs [in Coq.Lists.List]
NoDup_iff_ForallOrdPairs [in Coq.Lists.List]
NoDup_map_inv [in Coq.Lists.List]
NoDup_incl_NoDup [in Coq.Lists.List]
NoDup_length_incl [in Coq.Lists.List]
NoDup_incl_length [in Coq.Lists.List]
NoDup_nth [in Coq.Lists.List]
NoDup_nth_error [in Coq.Lists.List]
NoDup_count_occ' [in Coq.Lists.List]
NoDup_count_occ [in Coq.Lists.List]
nodup_inv [in Coq.Lists.List]
NoDup_nodup [in Coq.Lists.List]
nodup_incl [in Coq.Lists.List]
nodup_In [in Coq.Lists.List]
nodup_fixed_point [in Coq.Lists.List]
NoDup_filter [in Coq.Lists.List]
NoDup_rev [in Coq.Lists.List]
NoDup_app_remove_r [in Coq.Lists.List]
NoDup_app_remove_l [in Coq.Lists.List]
NoDup_app [in Coq.Lists.List]
NoDup_cons_iff [in Coq.Lists.List]
NoDup_remove_2 [in Coq.Lists.List]
NoDup_remove_1 [in Coq.Lists.List]
NoDup_remove [in Coq.Lists.List]
NoDup_Add [in Coq.Lists.List]
NoDup_dec [in Coq.Lists.ListDec]
NoDup_list_decidable [in Coq.Lists.ListDec]
NoDup_decidable [in Coq.Lists.ListDec]
NoDup_Permutation_bis [in Coq.Sorting.Permutation]
NoDup_Permutation [in Coq.Sorting.Permutation]
Noetherian_contains_Noetherian [in Coq.Sets.Relations_3_facts]
nonneg_derivative_0 [in Coq.Reals.Ranalysis1]
nonneg_derivative_1 [in Coq.Reals.MVT]
nonpos_derivative_1 [in Coq.Reals.MVT]
nonpos_derivative_0 [in Coq.Reals.MVT]
non_dep_dep_functional_rel_reification [in Coq.Logic.ChoiceFacts]
non_dep_dep_functional_choice [in Coq.Logic.ChoiceFacts]
Non_disjoint_union' [in Coq.Sets.Powerset_facts]
Non_disjoint_union [in Coq.Sets.Powerset_facts]
Noone_in_empty [in Coq.Sets.Constructive_sets]
NOrderProp.eq_0_gt_0_cases [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.le_pred_le_succ [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.le_succ_le_pred [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.le_pred_le [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.le_le_pred [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.le_pred_l [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.le_ind_rel [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.le_1_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.le_1_succ [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.le_0_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_pred_lt_succ [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_succ_lt_pred [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_pred_lt [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_pred_le [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_le_pred [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_lt_pred [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_pred_l [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_ind_rel [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_1_l' [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_lt_0 [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_1_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_0_succ [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.lt_wf_0 [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.measure_induction [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.neq_0_le_1 [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.neq_0_lt_0 [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.nle_succ_0 [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.nlt_0_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.pred_lt_mono [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.pred_le_mono [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.Private_strong_induction_le [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.succ_pred_pos [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderProp.zero_one [in Coq.Numbers.Natural.Abstract.NOrder]
NoRetractFromSmallPropositionToProp.mparadox [in Coq.Logic.Hurkens]
NoRetractFromSmallPropositionToProp.paradox [in Coq.Logic.Hurkens]
NoRetractFromTypeToProp.paradox [in Coq.Logic.Hurkens]
NoRetractToImpredicativeUniverse.paradox [in Coq.Logic.Hurkens]
NoRetractToModalProposition.modal [in Coq.Logic.Hurkens]
NoRetractToModalProposition.paradox [in Coq.Logic.Hurkens]
NoRetractToModalProposition.strength [in Coq.Logic.Hurkens]
NoRetractToNegativeProp.paradox [in Coq.Logic.Hurkens]
normalise_sound [in Coq.micromega.RingMicromega]
normalise_correct [in Coq.micromega.ZMicromega]
norm_app_int_norm [in Coq.Numbers.DecimalFacts]
norm_del_tail_int_norm [in Coq.Numbers.DecimalFacts]
norm_involutive [in Coq.Numbers.DecimalFacts]
norm_app_int [in Coq.Numbers.DecimalFacts]
norm_correct [in Coq.nsatz.NsatzTactic]
norm_subst_ok [in Coq.setoid_ring.Ring_polynom]
norm_subst_spec [in Coq.setoid_ring.Ring_polynom]
norm_aux_spec [in Coq.setoid_ring.Ring_polynom]
norm_aux_PEopp [in Coq.setoid_ring.Ring_polynom]
norm_aux_PEadd [in Coq.setoid_ring.Ring_polynom]
norm_aux_spec [in Coq.micromega.EnvRing]
norm_aux_PEopp [in Coq.micromega.EnvRing]
norm_aux_PEadd [in Coq.micromega.EnvRing]
norm_app_int_norm [in Coq.Numbers.HexadecimalFacts]
norm_del_tail_int_norm [in Coq.Numbers.HexadecimalFacts]
norm_involutive [in Coq.Numbers.HexadecimalFacts]
norm_app_int [in Coq.Numbers.HexadecimalFacts]
norm_subst_ok [in Coq.setoid_ring.Ncring_polynom]
norm_subst_spec [in Coq.setoid_ring.Ncring_polynom]
norm_aux_spec [in Coq.setoid_ring.Ncring_polynom]
norP [in Coq.ssr.ssrbool]
notin_flat_map_Forall [in Coq.Lists.List]
notin_remove [in Coq.Lists.List]
not_imp_rev_iff [in Coq.Logic.Decidable]
not_imp_iff [in Coq.Logic.Decidable]
not_and_iff [in Coq.Logic.Decidable]
not_or_iff [in Coq.Logic.Decidable]
not_not_iff [in Coq.Logic.Decidable]
not_false_iff [in Coq.Logic.Decidable]
not_true_iff [in Coq.Logic.Decidable]
not_iff [in Coq.Logic.Decidable]
not_imp [in Coq.Logic.Decidable]
not_and [in Coq.Logic.Decidable]
not_or [in Coq.Logic.Decidable]
not_not [in Coq.Logic.Decidable]
not_ex_not_all [in Coq.Logic.Classical_Pred_Type]
not_ex_all_not [in Coq.Logic.Classical_Pred_Type]
not_all_ex_not [in Coq.Logic.Classical_Pred_Type]
not_all_not_ex [in Coq.Logic.Classical_Pred_Type]
not_morph [in Coq.micromega.ZifyClasses]
not_Empty_Add [in Coq.Sets.Constructive_sets]
not_eq_S [in Coq.Init.Peano]
not_in_cons [in Coq.Lists.List]
not_lt [in Coq.Arith.Compare_dec]
not_ge [in Coq.Arith.Compare_dec]
not_gt [in Coq.Arith.Compare_dec]
not_le [in Coq.Arith.Compare_dec]
not_eq [in Coq.Arith.Compare_dec]
not_false_is_true [in Coq.ssr.ssrbool]
not_locked_false_eq_true [in Coq.ssr.ssreflect]
not_NoDup [in Coq.Lists.ListDec]
not_false_iff_true [in Coq.Bool.Bool]
not_true_iff_false [in Coq.Bool.Bool]
not_false_is_true [in Coq.Bool.Bool]
not_true_is_false [in Coq.Bool.Bool]
not_not_classic_set [in Coq.Logic.ClassicalUniqueChoice]
not_Zne [in Coq.ZArith.Zorder]
not_Zeq [in Coq.ZArith.Zorder]
not_Zeq_inf [in Coq.ZArith.ZArith_dec]
not_has_fixpoint [in Coq.Logic.Berardi]
not_hprop [in Coq.Logic.HLevels]
not_or_and [in Coq.Logic.Classical_Prop]
not_and_or [in Coq.Logic.Classical_Prop]
not_imply_elim2 [in Coq.Logic.Classical_Prop]
not_imply_elim [in Coq.Logic.Classical_Prop]
not_0_IZR [in Coq.Reals.RIneq]
not_IPR [in Coq.Reals.RIneq]
not_1_IPR [in Coq.Reals.RIneq]
not_1_INR [in Coq.Reals.RIneq]
not_INR [in Coq.Reals.RIneq]
not_0_INR [in Coq.Reals.RIneq]
not_injective_elim [in Coq.Sets.Image]
not_eq_sym [in Coq.Init.Logic]
not_iff_compat [in Coq.Init.Logic]
not_SIncl_empty [in Coq.Sets.Classical_sets]
not_empty_Inhabited [in Coq.Sets.Classical_sets]
not_included_empty_Inhabited [in Coq.Sets.Classical_sets]
not_prime_divide [in Coq.ZArith.Znumtheory]
not_prime_1 [in Coq.ZArith.Znumtheory]
not_prime_0 [in Coq.ZArith.Znumtheory]
not_rel_prime_0 [in Coq.ZArith.Znumtheory]
not_not_archimedean [in Coq.Reals.Rlogic]
not_make_conj_app [in Coq.micromega.Refl]
not_make_conj_cons [in Coq.micromega.Refl]
not_Rlt [in Coq.Reals.SeqProp]
no_fixpoint_negb [in Coq.Bool.Bool]
no_middle_eval_tt [in Coq.micromega.Tauto]
NParityProp.even_sub [in Coq.Numbers.Natural.Abstract.NParity]
NParityProp.even_pred [in Coq.Numbers.Natural.Abstract.NParity]
NParityProp.odd_sub [in Coq.Numbers.Natural.Abstract.NParity]
NParityProp.odd_pred [in Coq.Numbers.Natural.Abstract.NParity]
NPEadd_ok [in Coq.setoid_ring.Field_theory]
NPEmul_ok [in Coq.setoid_ring.Field_theory]
NPEopp_ok [in Coq.setoid_ring.Field_theory]
NPEpow_ok [in Coq.setoid_ring.Field_theory]
NPEsub_ok [in Coq.setoid_ring.Field_theory]
Nplus_reg_l [in Coq.NArith.BinNat]
NPowProp.even_pow [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.odd_pow [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_add_upper [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_add_lower [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_gt_lin_r [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_lower_bound [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_le_mono_r_iff [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_lt_mono_r_iff [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_le_mono_l_iff [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_lt_mono_l_iff [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_inj_r [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_inj_l [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_le_mono [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_le_mono_r [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_lt_mono_r [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_gt_1 [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_le_mono_l [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_lt_mono_l [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_eq_0_iff [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_nonzero [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_eq_0 [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_mul_r [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_mul_l [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_add_r [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_1_l [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_0_l [in Coq.Numbers.Natural.Abstract.NPow]
NPowProp.pow_succ_r' [in Coq.Numbers.Natural.Abstract.NPow]
nsatzR_diff [in Coq.nsatz.NsatzTactic]
Nseqe [in Coq.setoid_ring.InitialRing]
NSqrtProp.add_sqrt_le [in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_succ_or [in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_succ_le [in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_mul_above [in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_le_lin [in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_lt_square [in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_le_square [in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_square [in Coq.Numbers.Natural.Abstract.NSqrt]
NSqrtProp.sqrt_spec' [in Coq.Numbers.Natural.Abstract.NSqrt]
Nsth [in Coq.setoid_ring.InitialRing]
NStrongRecProp.strong_rec_any_fst_arg [in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec_0_any [in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec_fixpoint [in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec0_fixpoint [in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec0_more_steps [in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec_0 [in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec0_succ [in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec0_0 [in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecProp.strong_rec_alt [in Coq.Numbers.Natural.Abstract.NStrongRec]
NSubProp.add_dichotomy [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.add_sub_swap [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.add_sub_eq_nz [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.add_sub_eq_r [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.add_sub_eq_l [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.add_sub [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.add_sub_assoc [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.le_alt_dichotomy [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.le_equiv [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.le_add_le_sub_l [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.le_add_le_sub_r [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.le_sub_le_add_l [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.le_sub_le_add_r [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.le_sub_l [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.lt_equiv [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.lt_add_lt_sub_l [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.lt_add_lt_sub_r [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.lt_sub_lt_add_l [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.lt_sub_lt_add_r [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.mul_sub_distr_l [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.mul_sub_distr_r [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.mul_pred_r [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_sub_distr [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_le_mono_l [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_le_mono_r [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_lt [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_add_le [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_pred_r [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_pred_l [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_0_le [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_add_distr [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_add [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_succ_l [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_gt [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_diag [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_succ [in Coq.Numbers.Natural.Abstract.NSub]
NSubProp.sub_0_l [in Coq.Numbers.Natural.Abstract.NSub]
Nth [in Coq.setoid_ring.InitialRing]
ntheq_eqst [in Coq.Lists.Streams]
nth_map2 [in Coq.Vectors.VectorSpec]
nth_map [in Coq.Vectors.VectorSpec]
nth_order_replace_neq [in Coq.Vectors.VectorSpec]
nth_order_replace_eq [in Coq.Vectors.VectorSpec]
nth_replace_neq [in Coq.Vectors.VectorSpec]
nth_replace_eq [in Coq.Vectors.VectorSpec]
nth_append_R [in Coq.Vectors.VectorSpec]
nth_append_L [in Coq.Vectors.VectorSpec]
nth_order_ext [in Coq.Vectors.VectorSpec]
nth_order_last [in Coq.Vectors.VectorSpec]
nth_order_tl [in Coq.Vectors.VectorSpec]
nth_order_hd [in Coq.Vectors.VectorSpec]
nth_pred_double [in Coq.setoid_ring.BinList]
nth_jump [in Coq.setoid_ring.BinList]
nth_error_repeat [in Coq.Lists.List]
nth_repeat_lt [in Coq.Lists.List]
nth_repeat [in Coq.Lists.List]
nth_error_seq [in Coq.Lists.List]
nth_skipn [in Coq.Lists.List]
nth_error_skipn [in Coq.Lists.List]
nth_firstn [in Coq.Lists.List]
nth_error_firstn [in Coq.Lists.List]
nth_nth_nth_map [in Coq.Lists.List]
nth_error_map [in Coq.Lists.List]
nth_error_rev [in Coq.Lists.List]
nth_error_nth_None [in Coq.Lists.List]
nth_error_nth' [in Coq.Lists.List]
nth_error_nth [in Coq.Lists.List]
nth_error_cons_succ [in Coq.Lists.List]
nth_error_cons_0 [in Coq.Lists.List]
nth_error_S [in Coq.Lists.List]
nth_error_O [in Coq.Lists.List]
nth_error_cons [in Coq.Lists.List]
nth_error_nil [in Coq.Lists.List]
nth_error_ext [in Coq.Lists.List]
nth_error_app [in Coq.Lists.List]
nth_error_app2 [in Coq.Lists.List]
nth_error_app1 [in Coq.Lists.List]
nth_error_split [in Coq.Lists.List]
nth_error_Some [in Coq.Lists.List]
nth_error_None [in Coq.Lists.List]
nth_error_In [in Coq.Lists.List]
nth_ext [in Coq.Lists.List]
nth_split [in Coq.Lists.List]
nth_middle [in Coq.Lists.List]
nth_indep [in Coq.Lists.List]
nth_overflow [in Coq.Lists.List]
nth_In [in Coq.Lists.List]
nth_default_eq [in Coq.Lists.List]
nth_S_cons [in Coq.Lists.List]
nth_in_or_default [in Coq.Lists.List]
nth_pred_double [in Coq.micromega.Env]
nth_jump [in Coq.micromega.Env]
nth_spec [in Coq.micromega.Env]
nth_le [in Coq.Arith.Between]
Ntriv_div_th [in Coq.setoid_ring.InitialRing]
null_derivative_loc [in Coq.Reals.MVT]
null_derivative_1 [in Coq.Reals.MVT]
null_derivative_0 [in Coq.Reals.MVT]
nu_left_inv_on [in Coq.Logic.Eqdep_dec]
Nwadd_ok [in Coq.setoid_ring.InitialRing]
Nwmul_ok [in Coq.setoid_ring.InitialRing]
Nwopp_ok [in Coq.setoid_ring.InitialRing]
Nwscal_ok [in Coq.setoid_ring.InitialRing]
Nxor_eq_false [in Coq.NArith.Ndec]
Nxor_eq_true [in Coq.NArith.Ndec]
NZAddOrderProp.add_nonneg_cases [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_nonpos_cases [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_pos_cases [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_neg_cases [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_le_cases [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_lt_cases [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_nonneg_nonneg [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_nonneg_pos [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_pos_nonneg [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_pos_pos [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_le_lt_mono [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_lt_le_mono [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_le_mono [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_le_mono_r [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_le_mono_l [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_lt_mono [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_lt_mono_r [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.add_lt_mono_l [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.le_exists_sub [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.le_le_add_le [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.le_lt_add_lt [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.lt_le_add_lt [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.lt_add_pos_r [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderProp.lt_add_pos_l [in Coq.Numbers.NatInt.NZAddOrder]
NZAddProp.add_shuffle3 [in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_shuffle2 [in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_shuffle1 [in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_shuffle0 [in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_cancel_r [in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_cancel_l [in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_assoc [in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_1_r [in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_1_l [in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_comm [in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_succ_comm [in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_succ_r [in Coq.Numbers.NatInt.NZAdd]
NZAddProp.add_0_r [in Coq.Numbers.NatInt.NZAdd]
NZAddProp.sub_1_r [in Coq.Numbers.NatInt.NZAdd]
NZBaseProp.central_induction [in Coq.Numbers.NatInt.NZBase]
NZBaseProp.eq_stepl [in Coq.Numbers.NatInt.NZBase]
NZBaseProp.eq_sym_iff [in Coq.Numbers.NatInt.NZBase]
NZBaseProp.neq_sym [in Coq.Numbers.NatInt.NZBase]
NZBaseProp.succ_inj_wd_neg [in Coq.Numbers.NatInt.NZBase]
NZBaseProp.succ_inj_wd [in Coq.Numbers.NatInt.NZBase]
NZBaseProp.succ_inj [in Coq.Numbers.NatInt.NZBase]
NZCyclicAxiomsMod.add_succ_l [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.add_0_l [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.bi_induction [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.BS [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.B_holds [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.B0 [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.gt_wB_0 [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.gt_wB_1 [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.mul_succ_l [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.mul_0_l [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZ_to_Z_mod [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.one_succ [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.one_mod_wB [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.pred_succ [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.pred_mod_wB [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.sub_succ_r [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.sub_0_r [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.succ_mod_wB [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.two_succ [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.Zbounded_induction [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZDivProp.add_mul_mod_distr_r [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.add_mul_mod_distr_l [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.add_mod [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.add_mod_idemp_r [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.add_mod_idemp_l [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_mul_le [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_div [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_mul_cancel_l [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_mul_cancel_r [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_add_l [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_add [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_le_compat_l [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_le_lower_bound [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_le_upper_bound [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_lt_upper_bound [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_exact [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_le_mono [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_lt [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_str_pos_iff [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_small_iff [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_str_pos [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_pos [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_mul [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_1_l [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_1_r [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_0_l [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_small [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_same [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_unique_exact [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_unique [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.div_mod_unique [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_divides [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_mul_r [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_mod [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_add [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_small_iff [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_le [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_mul [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_1_l [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_1_r [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_0_l [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_small [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_same [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mod_unique [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mul_mod_distr_r [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mul_mod_distr_l [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mul_mod [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mul_mod_idemp_r [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mul_mod_idemp_l [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mul_succ_div_gt [in Coq.Numbers.NatInt.NZDiv]
NZDivProp.mul_div_le [in Coq.Numbers.NatInt.NZDiv]
NZDomainProp.bi_induction_pred [in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.central_induction_pred [in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.initial_ancestor [in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.initial_unique [in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.initial_alt2 [in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.initial_alt [in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.itersucc_or_iterpred [in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.itersucc_or_itersucc [in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.itersucc0_or_iterpred0 [in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.succ_onto_pred_injective [in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.succ_onto_gives_succ_pred [in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.succ_pred_approx [in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.succ_swap_pred [in Coq.Numbers.NatInt.NZDomain]
NZGcdProp.divide_gcd_iff [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_pos_le [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_factor_r [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_factor_l [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_mul_r [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_mul_l [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_add_r [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_antisym_nonneg [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_trans [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_refl [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_1_r_nonneg [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_0_l [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_0_r [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.divide_1_l [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.eq_mul_1_nonneg' [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.eq_mul_1_nonneg [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_mul_diag_l [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_eq_0 [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_eq_0_r [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_eq_0_l [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_diag_nonneg [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_1_r [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_1_l [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_0_r_nonneg [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_0_l_nonneg [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_assoc [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_comm [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_unique_alt [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_divide_iff [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.gcd_unique [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.mul_divide_cancel_r [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.mul_divide_cancel_l [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.mul_divide_mono_r [in Coq.Numbers.NatInt.NZGcd]
NZGcdProp.mul_divide_mono_l [in Coq.Numbers.NatInt.NZGcd]
nzhead_app_nzhead [in Coq.Numbers.DecimalFacts]
nzhead_del_tail_nzhead [in Coq.Numbers.DecimalFacts]
nzhead_del_tail_nzhead_eq [in Coq.Numbers.DecimalFacts]
nzhead_involutive [in Coq.Numbers.DecimalFacts]
nzhead_nonzero [in Coq.Numbers.DecimalFacts]
nzhead_iter_D0 [in Coq.Numbers.DecimalFacts]
nzhead_D0 [in Coq.Numbers.DecimalFacts]
nzhead_rev [in Coq.Numbers.DecimalFacts]
nzhead_revapp [in Coq.Numbers.DecimalFacts]
nzhead_revapp_0 [in Coq.Numbers.DecimalFacts]
nzhead_app_nil_l [in Coq.Numbers.DecimalFacts]
nzhead_app_nil [in Coq.Numbers.DecimalFacts]
nzhead_app_nil_r [in Coq.Numbers.DecimalFacts]
nzhead_app_r [in Coq.Numbers.DecimalFacts]
nzhead_app_l [in Coq.Numbers.DecimalFacts]
nzhead_spec [in Coq.Numbers.DecimalFacts]
nzhead_app_nzhead [in Coq.Numbers.HexadecimalFacts]
nzhead_del_tail_nzhead [in Coq.Numbers.HexadecimalFacts]
nzhead_del_tail_nzhead_eq [in Coq.Numbers.HexadecimalFacts]
nzhead_involutive [in Coq.Numbers.HexadecimalFacts]
nzhead_nonzero [in Coq.Numbers.HexadecimalFacts]
nzhead_iter_D0 [in Coq.Numbers.HexadecimalFacts]
nzhead_D0 [in Coq.Numbers.HexadecimalFacts]
nzhead_rev [in Coq.Numbers.HexadecimalFacts]
nzhead_revapp [in Coq.Numbers.HexadecimalFacts]
nzhead_revapp_0 [in Coq.Numbers.HexadecimalFacts]
nzhead_app_nil_l [in Coq.Numbers.HexadecimalFacts]
nzhead_app_nil [in Coq.Numbers.HexadecimalFacts]
nzhead_app_nil_r [in Coq.Numbers.HexadecimalFacts]
nzhead_app_r [in Coq.Numbers.HexadecimalFacts]
nzhead_app_l [in Coq.Numbers.HexadecimalFacts]
nzhead_spec [in Coq.Numbers.HexadecimalFacts]
NZLog2Prop.add_log2_lt [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_add_le [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_succ_double [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_eq_succ_iff_pow2 [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_eq_succ_is_pow2 [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_succ_or [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_succ_le [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_same [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_double [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_mul_pow2 [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_mul_above [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_mul_below [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_le_lin [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_lt_lin [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_lt_pow2 [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_le_pow2 [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_lt_cancel [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_le_mono [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_null [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_pos [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_2 [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_1 [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_pred_pow2 [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_pow2 [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_unique' [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_spec_alt [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_unique [in Coq.Numbers.NatInt.NZLog]
NZLog2Prop.log2_nonneg [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.add_log2_up_lt [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.le_log2_up_succ_log2 [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.le_log2_log2_up [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_add_le [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_succ_double [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_eq_succ_iff_pow2 [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_eq_succ_is_pow2 [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_succ_or [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_succ_le [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_same [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_double [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_mul_pow2 [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_mul_below [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_mul_above [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_le_lin [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_lt_lin [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_le_pow2 [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_lt_pow2 [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_lt_cancel [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_le_mono [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_null [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_pos [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_log2_up_exact [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_log2_up_spec [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_2 [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_1 [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_succ_pow2 [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_pow2 [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_unique [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_nonneg [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_nonpos [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_spec [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_eqn [in Coq.Numbers.NatInt.NZLog]
NZLog2UpProp.log2_up_eqn0 [in Coq.Numbers.NatInt.NZLog]
NZMulOrderProp.add_square_le [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.add_le_mul [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.crossmul_le_addsquare [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.eq_mul_0_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.eq_mul_0_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.eq_square_0 [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.eq_mul_0 [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.lt_0_mul [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.lt_1_mul_pos [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_2_mono_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_nonneg_cancel_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_nonneg_cancel_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_pos_cancel_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_pos_cancel_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_nonneg_nonneg [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_neg_pos [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_pos_neg [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_neg_neg [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_pos_pos [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_le_mono_nonneg [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_lt_mono_nonneg [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_le_mono_neg_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_le_mono_neg_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_le_mono_pos_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_le_mono_pos_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_id_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_id_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_cancel_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_cancel_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_le_mono_nonpos_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_le_mono_nonneg_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_le_mono_nonpos_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_le_mono_nonneg_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_lt_mono_neg_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_lt_mono_neg_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_lt_mono_pos_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_lt_mono_pos_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_lt_pred [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.neq_mul_0 [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.quadmul_le_squareadd [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.square_add_le [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.square_nonneg [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.square_le_simpl_nonneg [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.square_lt_simpl_nonneg [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.square_le_mono_nonneg [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.square_lt_mono_nonneg [in Coq.Numbers.NatInt.NZMulOrder]
NZMulProp.mul_shuffle3 [in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_shuffle2 [in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_shuffle1 [in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_shuffle0 [in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_1_r [in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_1_l [in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_assoc [in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_add_distr_l [in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_add_distr_r [in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_comm [in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_succ_r [in Coq.Numbers.NatInt.NZMul]
NZMulProp.mul_0_r [in Coq.Numbers.NatInt.NZMul]
NZOfNatOps.ofnat_sub [in Coq.Numbers.NatInt.NZDomain]
NZOfNatOps.ofnat_sub_r [in Coq.Numbers.NatInt.NZDomain]
NZOfNatOps.ofnat_mul [in Coq.Numbers.NatInt.NZDomain]
NZOfNatOps.ofnat_add [in Coq.Numbers.NatInt.NZDomain]
NZOfNatOps.ofnat_add_l [in Coq.Numbers.NatInt.NZDomain]
NZOfNatOrd.ofnat_le [in Coq.Numbers.NatInt.NZDomain]
NZOfNatOrd.ofnat_lt [in Coq.Numbers.NatInt.NZDomain]
NZOfNatOrd.ofnat_eq [in Coq.Numbers.NatInt.NZDomain]
NZOfNatOrd.ofnat_injective [in Coq.Numbers.NatInt.NZDomain]
NZOfNatOrd.ofnat_S_neq_0 [in Coq.Numbers.NatInt.NZDomain]
NZOfNatOrd.ofnat_S_gt_0 [in Coq.Numbers.NatInt.NZDomain]
NZOfNat.ofnat_pred [in Coq.Numbers.NatInt.NZDomain]
NZOfNat.ofnat_succ [in Coq.Numbers.NatInt.NZDomain]
NZOfNat.ofnat_zero [in Coq.Numbers.NatInt.NZDomain]
NZOrderProp.eq_dne [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.eq_decidable [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.eq_le_incl [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.gt_wf [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.left_induction' [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.left_induction [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_ind [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_dne [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_decidable [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_ngt [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_ge_cases [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_0_2 [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_0_1 [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_le_succ_r [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_succ_r [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_antisymm [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_lt_trans [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_stepr [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_stepl [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_neq [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_trans [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_gt_cases [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_succ_l [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_succ_diag_r [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.le_refl [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_ind [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_wf [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_succ_pred [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_exists_pred [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_nge [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_dne [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_decidable [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_gt_cases [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_ge_cases [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_1_l [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_0_2 [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_1_2 [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_0_1 [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_lt_succ_r [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_succ_l [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_le_trans [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_stepr [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_stepl [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_neq [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_trans [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_asymm [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_trichotomy [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_succ_diag_r [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.lt_le_incl [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.measure_left_induction [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.measure_right_induction [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.neq_succ_diag_r [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.neq_succ_diag_l [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.nle_gt [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.nle_succ_diag_l [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.nlt_succ_r [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.nlt_ge [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.nlt_succ_diag_l [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.order_induction'_0 [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.order_induction_0 [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.order_induction' [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.order_induction [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.right_induction' [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.right_induction [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.strong_left_induction' [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.strong_left_induction [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.strong_right_induction' [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.strong_right_induction [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.succ_le_mono [in Coq.Numbers.NatInt.NZOrder]
NZOrderProp.succ_lt_mono [in Coq.Numbers.NatInt.NZOrder]
Nzorn [in Coq.Reals.RiemannInt_SF]
NZParityProp.double_above [in Coq.Numbers.NatInt.NZParity]
NZParityProp.double_below [in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_odd [in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_even [in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_add_mul_2 [in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_add_mul_even [in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_add_even [in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_mul [in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_add [in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_succ_succ [in Coq.Numbers.NatInt.NZParity]
NZParityProp.Even_succ_succ [in Coq.Numbers.NatInt.NZParity]
NZParityProp.Even_succ [in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_succ [in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_2 [in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_1 [in Coq.Numbers.NatInt.NZParity]
NZParityProp.even_0 [in Coq.Numbers.NatInt.NZParity]
NZParityProp.Even_Odd_False [in Coq.Numbers.NatInt.NZParity]
NZParityProp.Even_or_Odd [in Coq.Numbers.NatInt.NZParity]
NZParityProp.negb_even [in Coq.Numbers.NatInt.NZParity]
NZParityProp.negb_odd [in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_odd [in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_even [in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_add_mul_2 [in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_add_mul_even [in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_add_even [in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_mul [in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_add [in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_succ_succ [in Coq.Numbers.NatInt.NZParity]
NZParityProp.Odd_succ_succ [in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_succ [in Coq.Numbers.NatInt.NZParity]
NZParityProp.Odd_succ [in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_2 [in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_1 [in Coq.Numbers.NatInt.NZParity]
NZParityProp.odd_0 [in Coq.Numbers.NatInt.NZParity]
NZParityProp.orb_even_odd [in Coq.Numbers.NatInt.NZParity]
NZPowProp.pow_add_upper [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_add_lower [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_gt_lin_r [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_le_mono_r_iff [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_lt_mono_r_iff [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_le_mono_l_iff [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_lt_mono_l_iff [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_inj_r [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_inj_l [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_lt_mono [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_le_mono [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_le_mono_r [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_lt_mono_r [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_gt_1 [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_le_mono_l [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_lt_mono_l [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_pos_nonneg [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_nonneg [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_mul_r [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_mul_l [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_add_r [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_eq_0_iff [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_nonzero [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_eq_0 [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_2_r [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_1_l [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_1_r [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_0_l' [in Coq.Numbers.NatInt.NZPow]
NZPowProp.pow_0_l [in Coq.Numbers.NatInt.NZPow]
NZSqrtProp.add_sqrt_le [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_add_le [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_eq_succ_iff_square [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_succ_or [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_succ_le [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_mul_above [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_mul_below [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_le_lin [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_lt_lin [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_pos [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_2 [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_1 [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_0 [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_lt_square [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_le_square [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_lt_cancel [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_le_mono [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_pred_square [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_square [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_unique' [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_spec_alt [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_unique [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_nonneg [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtProp.sqrt_spec_nonneg [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.add_sqrt_up_le [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.le_sqrt_up_succ_sqrt [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.le_sqrt_sqrt_up [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_add_le [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_eq_succ_iff_square [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_succ_or [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_succ_le [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_mul_below [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_mul_above [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_le_lin [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_lt_lin [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_pos [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_le_square [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_lt_square [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_lt_cancel [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_le_mono [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_sqrt_up_exact [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_sqrt_up_spec [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_2 [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_1 [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_0 [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_succ_square [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_square [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_unique [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_nonneg [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_spec [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_eqn [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtUpProp.sqrt_up_eqn0 [in Coq.Numbers.NatInt.NZSqrt]
nztail_involutive [in Coq.Numbers.DecimalFacts]
nztail_spec [in Coq.Numbers.DecimalFacts]
nztail_to_uint_pow10 [in Coq.Numbers.DecimalZ]
nztail_involutive [in Coq.Numbers.HexadecimalFacts]
nztail_spec [in Coq.Numbers.HexadecimalFacts]
nztail_to_hex_uint_pow16 [in Coq.Numbers.HexadecimalZ]
n_Sn [in Coq.Init.Peano]
N_ascii_bounded [in Coq.Strings.Ascii]
N_ascii_embedding [in Coq.Strings.Ascii]
N_nat_Z [in Coq.ZArith.Znat]
N.add_succ_l [in Coq.NArith.BinNat]
N.add_0_l [in Coq.NArith.BinNat]
N.binary_induction [in Coq.NArith.BinNat]
N.bi_induction [in Coq.NArith.BinNat]
N.compare_0_r [in Coq.NArith.BinNat]
N.compare_antisym [in Coq.NArith.BinNat]
N.compare_le_iff [in Coq.NArith.BinNat]
N.compare_lt_iff [in Coq.NArith.BinNat]
N.compare_eq_iff [in Coq.NArith.BinNat]
N.div_0_r [in Coq.NArith.BinNat]
N.div_mod' [in Coq.NArith.BinNat]
N.div_eucl_spec [in Coq.NArith.BinNat]
N.div2_succ_double [in Coq.NArith.BinNat]
N.div2_double [in Coq.NArith.BinNat]
N.double_le_mono [in Coq.NArith.BinNat]
N.double_lt_mono [in Coq.NArith.BinNat]
N.double_inj [in Coq.NArith.BinNat]
N.double_mul [in Coq.NArith.BinNat]
N.double_add [in Coq.NArith.BinNat]
N.double_spec [in Coq.NArith.BinNat]
N.eqb_eq [in Coq.NArith.BinNat]
N.even_spec [in Coq.NArith.BinNat]
N.gcd_nonneg [in Coq.NArith.BinNat]
N.gcd_greatest [in Coq.NArith.BinNat]
N.gcd_divide_r [in Coq.NArith.BinNat]
N.gcd_divide_l [in Coq.NArith.BinNat]
N.ge_le [in Coq.NArith.BinNat]
N.ge_le_iff [in Coq.NArith.BinNat]
N.ggcd_correct_divisors [in Coq.NArith.BinNat]
N.ggcd_gcd [in Coq.NArith.BinNat]
N.gt_lt [in Coq.NArith.BinNat]
N.gt_lt_iff [in Coq.NArith.BinNat]
N.iter_invariant [in Coq.NArith.BinNat]
N.iter_ind [in Coq.NArith.BinNat]
N.iter_add [in Coq.NArith.BinNat]
N.iter_succ_r [in Coq.NArith.BinNat]
N.iter_succ [in Coq.NArith.BinNat]
N.iter_swap [in Coq.NArith.BinNat]
N.iter_swap_gen [in Coq.NArith.BinNat]
N.land_spec [in Coq.NArith.BinNat]
N.ldiff_spec [in Coq.NArith.BinNat]
N.leb_le [in Coq.NArith.BinNat]
N.le_ge [in Coq.NArith.BinNat]
N.log2_nonpos [in Coq.NArith.BinNat]
N.log2_spec [in Coq.NArith.BinNat]
N.lor_spec [in Coq.NArith.BinNat]
N.ltb_lt [in Coq.NArith.BinNat]
N.lt_gt [in Coq.NArith.BinNat]
N.lt_succ_r [in Coq.NArith.BinNat]
N.lxor_spec [in Coq.NArith.BinNat]
N.max_r [in Coq.NArith.BinNat]
N.max_l [in Coq.NArith.BinNat]
N.min_r [in Coq.NArith.BinNat]
N.min_l [in Coq.NArith.BinNat]
N.mod_0_r [in Coq.NArith.BinNat]
N.mod_bound_pos [in Coq.NArith.BinNat]
N.mod_lt [in Coq.NArith.BinNat]
N.mul_succ_l [in Coq.NArith.BinNat]
N.mul_0_l [in Coq.NArith.BinNat]
N.odd_spec [in Coq.NArith.BinNat]
N.one_succ [in Coq.NArith.BinNat]
N.peano_rec_succ [in Coq.NArith.BinNat]
N.peano_rec_base [in Coq.NArith.BinNat]
N.peano_rect_succ [in Coq.NArith.BinNat]
N.peano_rect_base [in Coq.NArith.BinNat]
N.pos_pred_shiftl_high [in Coq.NArith.BinNat]
N.pos_pred_shiftl_low [in Coq.NArith.BinNat]
N.pos_ldiff_spec [in Coq.NArith.BinNat]
N.pos_land_spec [in Coq.NArith.BinNat]
N.pos_lor_spec [in Coq.NArith.BinNat]
N.pos_lxor_spec [in Coq.NArith.BinNat]
N.pos_div_eucl_remainder [in Coq.NArith.BinNat]
N.pos_div_eucl_spec [in Coq.NArith.BinNat]
N.pos_pred_succ [in Coq.NArith.BinNat]
N.pos_pred_spec [in Coq.NArith.BinNat]
N.pow_neg_r [in Coq.NArith.BinNat]
N.pow_succ_r [in Coq.NArith.BinNat]
N.pow_0_r [in Coq.NArith.BinNat]
N.pred_div2_up [in Coq.NArith.BinNat]
N.pred_sub [in Coq.NArith.BinNat]
N.pred_succ [in Coq.NArith.BinNat]
N.recursion_succ [in Coq.NArith.BinNat]
N.recursion_0 [in Coq.NArith.BinNat]
N.shiftl_spec_low [in Coq.NArith.BinNat]
N.shiftl_spec_high [in Coq.NArith.BinNat]
N.shiftl_succ_r [in Coq.NArith.BinNat]
N.shiftr_spec [in Coq.NArith.BinNat]
N.shiftr_succ_r [in Coq.NArith.BinNat]
N.size_le [in Coq.NArith.BinNat]
N.size_gt [in Coq.NArith.BinNat]
N.size_log2 [in Coq.NArith.BinNat]
N.sqrtrem_spec [in Coq.NArith.BinNat]
N.sqrtrem_sqrt [in Coq.NArith.BinNat]
N.sqrt_neg [in Coq.NArith.BinNat]
N.sqrt_spec [in Coq.NArith.BinNat]
N.square_spec [in Coq.NArith.BinNat]
N.strong_induction_le [in Coq.NArith.BinNat]
N.sub_succ_r [in Coq.NArith.BinNat]
N.sub_0_r [in Coq.NArith.BinNat]
N.succ_double_le_mono [in Coq.NArith.BinNat]
N.succ_double_lt_mono [in Coq.NArith.BinNat]
N.succ_double_lt [in Coq.NArith.BinNat]
N.succ_double_inj [in Coq.NArith.BinNat]
N.succ_double_mul [in Coq.NArith.BinNat]
N.succ_double_add [in Coq.NArith.BinNat]
N.succ_double_spec [in Coq.NArith.BinNat]
N.succ_0_discr [in Coq.NArith.BinNat]
N.succ_pos_pred [in Coq.NArith.BinNat]
N.succ_pos_spec [in Coq.NArith.BinNat]
N.testbit_neg_r [in Coq.NArith.BinNat]
N.testbit_even_succ [in Coq.NArith.BinNat]
N.testbit_odd_succ [in Coq.NArith.BinNat]
N.testbit_succ_r_div2 [in Coq.NArith.BinNat]
N.testbit_odd_0 [in Coq.NArith.BinNat]
N.testbit_even_0 [in Coq.NArith.BinNat]
N.two_succ [in Coq.NArith.BinNat]
N2Nat.id [in Coq.NArith.Nnat]
N2Nat.inj [in Coq.NArith.Nnat]
N2Nat.inj_iter [in Coq.NArith.Nnat]
N2Nat.inj_min [in Coq.NArith.Nnat]
N2Nat.inj_max [in Coq.NArith.Nnat]
N2Nat.inj_pow [in Coq.NArith.Nnat]
N2Nat.inj_mod [in Coq.NArith.Nnat]
N2Nat.inj_div [in Coq.NArith.Nnat]
N2Nat.inj_compare [in Coq.NArith.Nnat]
N2Nat.inj_div2 [in Coq.NArith.Nnat]
N2Nat.inj_pred [in Coq.NArith.Nnat]
N2Nat.inj_sub [in Coq.NArith.Nnat]
N2Nat.inj_mul [in Coq.NArith.Nnat]
N2Nat.inj_add [in Coq.NArith.Nnat]
N2Nat.inj_succ [in Coq.NArith.Nnat]
N2Nat.inj_succ_double [in Coq.NArith.Nnat]
N2Nat.inj_double [in Coq.NArith.Nnat]
N2Nat.inj_0 [in Coq.NArith.Nnat]
N2Nat.inj_iff [in Coq.NArith.Nnat]
N2Z.id [in Coq.ZArith.Znat]
N2Z.inj [in Coq.ZArith.Znat]
N2Z.inj_testbit [in Coq.ZArith.Znat]
N2Z.inj_pow [in Coq.ZArith.Znat]
N2Z.inj_quot2 [in Coq.ZArith.Znat]
N2Z.inj_div2 [in Coq.ZArith.Znat]
N2Z.inj_rem [in Coq.ZArith.Znat]
N2Z.inj_quot [in Coq.ZArith.Znat]
N2Z.inj_mod [in Coq.ZArith.Znat]
N2Z.inj_div [in Coq.ZArith.Znat]
N2Z.inj_max [in Coq.ZArith.Znat]
N2Z.inj_min [in Coq.ZArith.Znat]
N2Z.inj_pred [in Coq.ZArith.Znat]
N2Z.inj_pred_max [in Coq.ZArith.Znat]
N2Z.inj_succ [in Coq.ZArith.Znat]
N2Z.inj_sub [in Coq.ZArith.Znat]
N2Z.inj_sub_max [in Coq.ZArith.Znat]
N2Z.inj_mul [in Coq.ZArith.Znat]
N2Z.inj_add [in Coq.ZArith.Znat]
N2Z.inj_abs_N [in Coq.ZArith.Znat]
N2Z.inj_gt [in Coq.ZArith.Znat]
N2Z.inj_ge [in Coq.ZArith.Znat]
N2Z.inj_lt [in Coq.ZArith.Znat]
N2Z.inj_le [in Coq.ZArith.Znat]
N2Z.inj_compare [in Coq.ZArith.Znat]
N2Z.inj_pos [in Coq.ZArith.Znat]
N2Z.inj_0 [in Coq.ZArith.Znat]
N2Z.inj_iff [in Coq.ZArith.Znat]
N2Z.is_nonneg [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 | (25958 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 | (999 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 | (811 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 | (1769 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 | (587 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 | (11879 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 | (960 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (508 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (307 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (479 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (495 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 | (905 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 | (1199 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 | (4894 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (166 entries) |