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 | (72652 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 | (1040 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 | (47157 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 | (790 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 | (1547 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 | (588 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 | (11857 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 | (1030 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 | (634 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (308 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (474 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 | (492 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 | (881 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 | (1439 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 | (4250 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 | (165 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_Npow [in Coq.NArith.Nnat]

nat_of_Nmod [in Coq.NArith.Nnat]

nat_of_Ndiv [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]

negbE [in Coq.Numbers.Cyclic.Int63.Int63]

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]

null [in Coq.micromega.Tauto]

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_pow [in Coq.NArith.Nnat]

N_of_nat_mod [in Coq.NArith.Nnat]

N_of_nat_div [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 | (72652 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 | (1040 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 | (47157 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 | (790 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 | (1547 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 | (588 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 | (11857 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 | (1030 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 | (634 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (308 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (474 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 | (492 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 | (881 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 | (1439 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 | (4250 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 | (165 entries) |