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 | (21801 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 | (910 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 | (729 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 | (1464 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 | (494 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 | (10179 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 | (676 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 | (537 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 | (374 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 | (287 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 | (457 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 | (616 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 | (1332 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 | (3609 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 | (137 entries) |

## N (abbreviation)

nat_of_N_of_nat [in Coq.NArith.Nnat]nat_of_Nmin [in Coq.NArith.Nnat]

nat_of_Nmax [in Coq.NArith.Nnat]

nat_of_Ncompare [in Coq.NArith.Nnat]

nat_of_Ndiv2 [in Coq.NArith.Nnat]

nat_of_Npred [in Coq.NArith.Nnat]

nat_of_Nminus [in Coq.NArith.Nnat]

nat_of_Nmult [in Coq.NArith.Nnat]

nat_of_Nplus [in Coq.NArith.Nnat]

nat_of_Nsucc [in Coq.NArith.Nnat]

nat_of_Ndouble_plus_one [in Coq.NArith.Nnat]

nat_of_Ndouble [in Coq.NArith.Nnat]

nat_of_N_inj [in Coq.NArith.Nnat]

nat_of_P [in Coq.PArith.BinPos]

nat_of_N [in Coq.NArith.BinNat]

nat_of_P_o_P_of_succ_nat_eq_succ [in Coq.PArith.Pnat]

nat_of_P_compare_morphism [in Coq.PArith.Pnat]

nat_of_P_mult_morphism [in Coq.PArith.Pnat]

nat_of_P_plus_morphism [in Coq.PArith.Pnat]

nat_of_P_succ_morphism [in Coq.PArith.Pnat]

nat_of_P_of_succ_nat [in Coq.PArith.Pnat]

nat_of_P_inj [in Coq.PArith.Pnat]

nat_of_P_inj_iff [in Coq.PArith.Pnat]

nat_of_P_pos [in Coq.PArith.Pnat]

nat_of_P_is_S [in Coq.PArith.Pnat]

nat_of_P_xI [in Coq.PArith.Pnat]

nat_of_P_xO [in Coq.PArith.Pnat]

nat_of_P_xH [in Coq.PArith.Pnat]

nat_compare_S [in Coq.Arith.Compare_dec]

nat_compare_eq_iff [in Coq.Arith.Compare_dec]

nat_compare_spec [in Coq.Arith.Compare_dec]

nat_compare [in Coq.Arith.Compare_dec]

Nbit [in Coq.NArith.Ndigits]

NBitsProp.lnextcarry [in Coq.Numbers.Natural.Abstract.NBits]

NBitsProp.lxor3 [in Coq.Numbers.Natural.Abstract.NBits]

NBitsProp.nextcarry [in Coq.Numbers.Natural.Abstract.NBits]

NBitsProp.xor3 [in Coq.Numbers.Natural.Abstract.NBits]

Nbit0 [in Coq.NArith.Ndigits]

Ncompare [in Coq.NArith.BinNat]

Ncompare_0 [in Coq.NArith.BinNat]

Ncompare_spec [in Coq.NArith.BinNat]

Ncompare_eq_correct [in Coq.NArith.BinNat]

Ncompare_Eq_eq [in Coq.NArith.BinNat]

Ncompare_refl [in Coq.NArith.BinNat]

Ndiscr [in Coq.NArith.BinNat]

Ndiv [in Coq.NArith.Ndiv_def]

Ndivide [in Coq.NArith.Ngcd_def]

Ndiv_mod_eq [in Coq.NArith.Ndiv_def]

Ndiv_eucl_correct [in Coq.NArith.Ndiv_def]

Ndiv_eucl [in Coq.NArith.Ndiv_def]

Ndiv_Zquot [in Coq.ZArith.Zquot]

Ndiv2 [in Coq.NArith.BinNat]

Ndouble [in Coq.NArith.BinNat]

Ndouble_plus_one_inj [in Coq.NArith.BinNat]

Ndouble_inj [in Coq.NArith.BinNat]

Ndouble_plus_one_div2 [in Coq.NArith.BinNat]

Ndouble_div2 [in Coq.NArith.BinNat]

Ndouble_plus_one [in Coq.NArith.BinNat]

negb_intro [in Coq.Bool.Bool]

negb_elim [in Coq.Bool.Bool]

Neqb [in Coq.NArith.BinNat]

Neqb [in Coq.NArith.Ndec]

Neqb_eq [in Coq.NArith.BinNat]

Neqb_comm [in Coq.NArith.Ndec]

Neqb_correct [in Coq.NArith.Ndec]

neq_O_lt [in Coq.Arith.Lt]

Neven [in Coq.NArith.BinNat]

Neven_spec [in Coq.NArith.BinNat]

Ngcd [in Coq.NArith.Ngcd_def]

Ngcd_greatest [in Coq.NArith.Ngcd_def]

Ngcd_divide_r [in Coq.NArith.Ngcd_def]

Ngcd_divide_l [in Coq.NArith.Ngcd_def]

Nge [in Coq.NArith.BinNat]

Nggcd [in Coq.NArith.Ngcd_def]

Nggcd_correct_divisors [in Coq.NArith.Ngcd_def]

Nggcd_gcd [in Coq.NArith.Ngcd_def]

Ngt [in Coq.NArith.BinNat]

Ngt_Nlt [in Coq.NArith.BinNat]

nil [in Coq.Lists.List]

nil_sort [in Coq.Sorting.Sorted]

nil_leA [in Coq.Sorting.Sorted]

Nind [in Coq.NArith.BinNat]

Ninterp_PElist [in Coq.setoid_ring.Field_theory]

Nle [in Coq.NArith.BinNat]

Nle_succ_l [in Coq.NArith.BinNat]

Nle_trans [in Coq.NArith.BinNat]

Nle_lteq [in Coq.NArith.BinNat]

Nle_0 [in Coq.NArith.BinNat]

Nlog2 [in Coq.NArith.BinNat]

Nlog2_nonpos [in Coq.NArith.BinNat]

Nlog2_spec [in Coq.NArith.BinNat]

Nlt [in Coq.NArith.BinNat]

Nlt_not_eq [in Coq.NArith.BinNat]

Nlt_succ_r [in Coq.NArith.BinNat]

Nlt_trans [in Coq.NArith.BinNat]

Nlt_irrefl [in Coq.NArith.BinNat]

Nmax [in Coq.NArith.BinNat]

Nmin [in Coq.NArith.BinNat]

Nminus [in Coq.NArith.BinNat]

Nminus_succ_r [in Coq.NArith.BinNat]

Nminus_0_r [in Coq.NArith.BinNat]

Nminus_N0_Nle [in Coq.NArith.BinNat]

Nmin_choice [in Coq.NArith.Ndec]

Nmk_monpol_list [in Coq.setoid_ring.Field_theory]

Nmod [in Coq.NArith.Ndiv_def]

Nmod_lt [in Coq.NArith.Ndiv_def]

Nmod_Zrem [in Coq.ZArith.Zquot]

NMulOrderProp.mul_pos [in Coq.Numbers.Natural.Abstract.NMulOrder]

Nmult [in Coq.NArith.BinNat]

Nmult_plus_distr_r [in Coq.NArith.BinNat]

Nmult_assoc [in Coq.NArith.BinNat]

Nmult_comm [in Coq.NArith.BinNat]

Nmult_1_r [in Coq.NArith.BinNat]

Nmult_1_l [in Coq.NArith.BinNat]

Nmult_0_l [in Coq.NArith.BinNat]

Nnorm [in Coq.setoid_ring.Field_theory]

Nodd [in Coq.NArith.BinNat]

Nodd_spec [in Coq.NArith.BinNat]

nosimpl [in Coq.ssr.ssreflect]

not_O_IZR [in Coq.Reals.RIneq]

not_O_INR [in Coq.Reals.RIneq]

not_INR_O [in Coq.Reals.RIneq]

not_nm_INR [in Coq.Reals.RIneq]

not_eq_sym [in Coq.Arith.Compare]

NPEeval [in Coq.setoid_ring.Field_theory]

Nplus [in Coq.NArith.BinNat]

Nplus_succ [in Coq.NArith.BinNat]

Nplus_assoc [in Coq.NArith.BinNat]

Nplus_comm [in Coq.NArith.BinNat]

Nplus_0_r [in Coq.NArith.BinNat]

Nplus_0_l [in Coq.NArith.BinNat]

Npos [in Coq.NArith.BinNat]

Npow [in Coq.NArith.BinNat]

Npow_succ_r [in Coq.NArith.BinNat]

Npow_0_r [in Coq.NArith.BinNat]

NPphi_pow [in Coq.setoid_ring.Field_theory]

NPphi_dev [in Coq.setoid_ring.Field_theory]

Npred [in Coq.NArith.BinNat]

Npred_minus [in Coq.NArith.BinNat]

Npred_succ [in Coq.NArith.BinNat]

NProp [in Coq.Logic.ClassicalFacts]

Nrec [in Coq.NArith.BinNat]

Nrect [in Coq.NArith.BinNat]

Nrect_step [in Coq.NArith.BinNat]

Nrect_base [in Coq.NArith.BinNat]

Nrec_succ [in Coq.NArith.BinNat]

Nrec_base [in Coq.NArith.BinNat]

Nsize [in Coq.NArith.Ndigits]

Nsqrt [in Coq.NArith.Nsqrt_def]

Nsqrtrem [in Coq.NArith.Nsqrt_def]

Nsqrtrem_sqrt [in Coq.NArith.Nsqrt_def]

Nsqrtrem_spec [in Coq.NArith.Nsqrt_def]

Nsqrt_spec [in Coq.NArith.Nsqrt_def]

Nsucc [in Coq.NArith.BinNat]

Nsucc_inj [in Coq.NArith.BinNat]

Nsucc_0 [in Coq.NArith.BinNat]

Nsucc_pos_spec [in Coq.NArith.BinNat]

Nsucc_pred [in Coq.NArith.BinNat]

Nsucc_pos [in Coq.NArith.BinNat]

Nxor [in Coq.NArith.Ndigits]

Nxor_nilpotent [in Coq.NArith.Ndigits]

Nxor_neutral_right [in Coq.NArith.Ndigits]

Nxor_neutral_left [in Coq.NArith.Ndigits]

Nxor_assoc [in Coq.NArith.Ndigits]

Nxor_comm [in Coq.NArith.Ndigits]

Nxor_eq [in Coq.NArith.Ndigits]

NZCyclicAxiomsMod.P [in Coq.Numbers.Cyclic.Abstract.NZCyclic]

NZCyclicAxiomsMod.S [in Coq.Numbers.Cyclic.Abstract.NZCyclic]

NZCyclicAxiomsMod.wB [in Coq.Numbers.Cyclic.Abstract.NZCyclic]

NZOrderProp.lt_ngt [in Coq.Numbers.NatInt.NZOrder]

NZOrderProp.lt_eq_gt_cases [in Coq.Numbers.NatInt.NZOrder]

N_of_max [in Coq.NArith.Nnat]

N_of_min [in Coq.NArith.Nnat]

N_of_nat_compare [in Coq.NArith.Nnat]

N_of_div2 [in Coq.NArith.Nnat]

N_of_mult [in Coq.NArith.Nnat]

N_of_minus [in Coq.NArith.Nnat]

N_of_plus [in Coq.NArith.Nnat]

N_of_pred [in Coq.NArith.Nnat]

N_of_S [in Coq.NArith.Nnat]

N_of_double_plus_one [in Coq.NArith.Nnat]

N_of_double [in Coq.NArith.Nnat]

N_of_nat_inj [in Coq.NArith.Nnat]

N_of_nat_of_N [in Coq.NArith.Nnat]

N_of_Z [in Coq.setoid_ring.ZArithRing]

N_eq_dec [in Coq.NArith.BinNat]

N_of_nat [in Coq.NArith.BinNat]

N_ind [in Coq.NArith.BinNat]

N_rec [in Coq.NArith.BinNat]

N_rect [in Coq.NArith.BinNat]

n_of_Z [in Coq.micromega.ZMicromega]

N.pos [in Coq.NArith.BinNatDef]

N0 [in Coq.NArith.BinNat]

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 | (21801 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 | (910 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 | (729 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 | (1464 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 | (494 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 | (10179 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 | (676 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 | (537 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 | (374 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 | (287 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 | (457 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 | (616 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 | (1332 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 | (3609 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 | (137 entries) |