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 | (68863 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 | (985 entries) |

Binder 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 | (44709 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 | (761 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 | (1497 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 | (570 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 | (11380 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 | (976 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 | (603 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 | (298 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 | (460 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 | (476 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 | (811 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 | (1157 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 | (4018 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 | (162 entries) |

## N (abbreviation)

nat_of_P [in Coq.PArith.BinPos]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_of_N [in Coq.NArith.BinNat]

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]

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_0 [in Coq.NArith.BinNat]

Ncompare_eq_correct [in Coq.NArith.BinNat]

Ncompare_Eq_eq [in Coq.NArith.BinNat]

Ndivide [in Coq.NArith.Ngcd_def]

Ndiv_Zquot [in Coq.ZArith.Zquot]

Ndiv_mod_eq [in Coq.NArith.Ndiv_def]

Ndiv_eucl_correct [in Coq.NArith.Ndiv_def]

Ndouble_plus_one_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_comm [in Coq.NArith.Ndec]

Neqb_correct [in Coq.NArith.Ndec]

neq_O_lt [in Coq.Arith.Lt]

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]

Nggcd [in Coq.NArith.Ngcd_def]

Nggcd_correct_divisors [in Coq.NArith.Ngcd_def]

Nggcd_gcd [in Coq.NArith.Ngcd_def]

Ngt_Nlt [in Coq.NArith.BinNat]

nil [in Coq.Lists.List]

nil [in Coq.Reals.RList]

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_lteq [in Coq.NArith.BinNat]

Nle_0 [in Coq.NArith.BinNat]

Nlt_not_eq [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_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]

NonPropType.Exports.nonPropType [in Coq.ssr.ssreflect]

NonPropType.Exports.notProp [in Coq.ssr.ssreflect]

nosimpl [in Coq.ssr.ssreflect]

not_eq_sym [in Coq.Arith.Compare]

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]

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]

NPphi_pow [in Coq.setoid_ring.Field_theory]

NPphi_dev [in Coq.setoid_ring.Field_theory]

Npred_minus [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_spec [in Coq.NArith.Nsqrt_def]

Nsucc_0 [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_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_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_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 | (68863 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 | (985 entries) |

Binder 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 | (44709 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 | (761 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 | (1497 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 | (570 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 | (11380 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 | (976 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 | (603 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 | (298 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 | (460 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 | (476 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 | (811 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 | (1157 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 | (4018 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 | (162 entries) |