Standard Library | The Coq Proof Assistant

Global Index

(26071 entries)

Notation Index

F

J

K

T

X

Y

_

(1003 entries)

Module Index

J

X

Y

_

other

(815 entries)

Variable Index

J

Q

V

X

Y

_

other

(1771 entries)

Library Index

K

X

Y

_

other

(589 entries)

Constructor Index

K

Y

_

other

(961 entries)

Lemma Index

other

(12021 entries)

Axiom Index

J

K

V

X

Y

_

other

(508 entries)

Inductive Index

X

Y

_

other

(308 entries)

Projection Index

G

K

X

Y

_

other

(479 entries)

Section Index

J

Q

X

Y

_

other

(496 entries)

Instance Index

J

V

X

Y

_

other

(906 entries)

Abbreviation Index

J

Y

_

other

(1204 entries)

Definition Index

_

other

(4844 entries)

Record Index

J

X

Y

_

other

(166 entries)

N (abbreviation)

nat_of_P [in Stdlib.PArith.BinPos]
nat_of_P_o_P_of_succ_nat_eq_succ [in Stdlib.PArith.Pnat]
nat_of_P_compare_morphism [in Stdlib.PArith.Pnat]
nat_of_P_mult_morphism [in Stdlib.PArith.Pnat]
nat_of_P_plus_morphism [in Stdlib.PArith.Pnat]
nat_of_P_succ_morphism [in Stdlib.PArith.Pnat]
nat_of_P_of_succ_nat [in Stdlib.PArith.Pnat]
nat_of_P_inj [in Stdlib.PArith.Pnat]
nat_of_P_inj_iff [in Stdlib.PArith.Pnat]
nat_of_P_pos [in Stdlib.PArith.Pnat]
nat_of_P_is_S [in Stdlib.PArith.Pnat]
nat_of_P_xI [in Stdlib.PArith.Pnat]
nat_of_P_xO [in Stdlib.PArith.Pnat]
nat_of_P_xH [in Stdlib.PArith.Pnat]
nat_of_N [in Stdlib.NArith.BinNat]
nat_compare_S [in Stdlib.Arith.Compare_dec]
nat_of_N_of_nat [in Stdlib.NArith.Nnat]
nat_of_Nmin [in Stdlib.NArith.Nnat]
nat_of_Nmax [in Stdlib.NArith.Nnat]
nat_of_Npow [in Stdlib.NArith.Nnat]
nat_of_Nmod [in Stdlib.NArith.Nnat]
nat_of_Ndiv [in Stdlib.NArith.Nnat]
nat_of_Ncompare [in Stdlib.NArith.Nnat]
nat_of_Ndiv2 [in Stdlib.NArith.Nnat]
nat_of_Npred [in Stdlib.NArith.Nnat]
nat_of_Nminus [in Stdlib.NArith.Nnat]
nat_of_Nmult [in Stdlib.NArith.Nnat]
nat_of_Nplus [in Stdlib.NArith.Nnat]
nat_of_Nsucc [in Stdlib.NArith.Nnat]
nat_of_Ndouble_plus_one [in Stdlib.NArith.Nnat]
nat_of_Ndouble [in Stdlib.NArith.Nnat]
nat_of_N_inj [in Stdlib.NArith.Nnat]
NBitsProp.lnextcarry [in Stdlib.Numbers.Natural.Abstract.NBits]
NBitsProp.lxor3 [in Stdlib.Numbers.Natural.Abstract.NBits]
NBitsProp.nextcarry [in Stdlib.Numbers.Natural.Abstract.NBits]
NBitsProp.xor3 [in Stdlib.Numbers.Natural.Abstract.NBits]
Ncompare_0 [in Stdlib.NArith.BinNat]
Ncompare_eq_correct [in Stdlib.NArith.BinNat]
Ncompare_Eq_eq [in Stdlib.NArith.BinNat]
Ndivide [in Stdlib.NArith.Ngcd_def]
NDivProp0.add_mod [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.add_mod_idemp_r [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.add_mod_idemp_l [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_mul_le [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_div [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_mul_cancel_l [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_mul_cancel_r [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_le_upper_bound [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_lt_upper_bound [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_exact [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_le_mono [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.div_0_l [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mod_divides [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mod_mul_r [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mod_mod [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mod_add [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mod_le [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mod_mul [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mod_0_l [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mod_same [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mod_eq [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mul_mod [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mul_mod_idemp_r [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mul_mod_idemp_l [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mul_mod_distr_l [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mul_mod_distr_r [in Stdlib.Numbers.Natural.Abstract.NDiv0]
NDivProp0.mul_div_le [in Stdlib.Numbers.Natural.Abstract.NDiv0]
Ndiv_Zquot [in Stdlib.ZArith.Zquot]
Ndiv_mod_eq [in Stdlib.NArith.Ndiv_def]
Ndiv_eucl_correct [in Stdlib.NArith.Ndiv_def]
Ndouble_plus_one_inj [in Stdlib.NArith.BinNat]
Ndouble_plus_one_div2 [in Stdlib.NArith.BinNat]
Ndouble_div2 [in Stdlib.NArith.BinNat]
Ndouble_plus_one [in Stdlib.NArith.BinNat]
negb_intro [in Stdlib.Bool.Bool]
negb_elim [in Stdlib.Bool.Bool]
Neqb_comm [in Stdlib.NArith.Ndec]
Neqb_correct [in Stdlib.NArith.Ndec]
Ngcd [in Stdlib.NArith.Ngcd_def]
NGcdProp.divide_gcd_iff' [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.divide_antisym_nonneg [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_unique_alt' [in Stdlib.Numbers.Natural.Abstract.NGcd]
NGcdProp.gcd_unique' [in Stdlib.Numbers.Natural.Abstract.NGcd]
Ngcd_greatest [in Stdlib.NArith.Ngcd_def]
Ngcd_divide_r [in Stdlib.NArith.Ngcd_def]
Ngcd_divide_l [in Stdlib.NArith.Ngcd_def]
Nggcd [in Stdlib.NArith.Ngcd_def]
Nggcd_correct_divisors [in Stdlib.NArith.Ngcd_def]
Nggcd_gcd [in Stdlib.NArith.Ngcd_def]
Ngt_Nlt [in Stdlib.NArith.BinNat]
nil [in Stdlib.Lists.List]
nil_sort [in Stdlib.Sorting.Sorted]
nil_leA [in Stdlib.Sorting.Sorted]
Nind [in Stdlib.NArith.BinNat]
Ninterp_PElist [in Stdlib.setoid_ring.Field_theory]
NLcmProp0.divide_div [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.divide_div_mul_exact [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.gcd_mod [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.gcd_div_factor [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.lcm_unique_alt [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.lcm_unique [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.lcm_equiv2 [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.lcm_equiv1 [in Stdlib.Numbers.Natural.Abstract.NLcm0]
NLcmProp0.mod_divide [in Stdlib.Numbers.Natural.Abstract.NLcm0]
Nle_lteq [in Stdlib.NArith.BinNat]
Nle_0 [in Stdlib.NArith.BinNat]
Nlt_not_eq [in Stdlib.NArith.BinNat]
Nminus [in Stdlib.NArith.BinNat]
Nminus_succ_r [in Stdlib.NArith.BinNat]
Nminus_0_r [in Stdlib.NArith.BinNat]
Nminus_N0_Nle [in Stdlib.NArith.BinNat]
Nmin_choice [in Stdlib.NArith.Ndec]
Nmk_monpol_list [in Stdlib.setoid_ring.Field_theory]
Nmod [in Stdlib.NArith.Ndiv_def]
Nmod_Zrem [in Stdlib.ZArith.Zquot]
NMulOrderProp.mul_pos [in Stdlib.Numbers.Natural.Abstract.NMulOrder]
Nmult [in Stdlib.NArith.BinNat]
Nmult_plus_distr_r [in Stdlib.NArith.BinNat]
Nmult_assoc [in Stdlib.NArith.BinNat]
Nmult_comm [in Stdlib.NArith.BinNat]
Nmult_1_r [in Stdlib.NArith.BinNat]
Nmult_1_l [in Stdlib.NArith.BinNat]
Nmult_0_l [in Stdlib.NArith.BinNat]
Nnorm [in Stdlib.setoid_ring.Field_theory]
NonPropType.Exports.nonPropType [in Stdlib.ssr.ssreflect]
NonPropType.Exports.notProp [in Stdlib.ssr.ssreflect]
nosimpl [in Stdlib.ssr.ssreflect]
not_identity_sym [in Stdlib.Init.Datatypes]
not_eq_sym [in Stdlib.Arith.Compare]
not_O_IZR [in Stdlib.Reals.RIneq]
not_O_INR [in Stdlib.Reals.RIneq]
not_INR_O [in Stdlib.Reals.RIneq]
not_nm_INR [in Stdlib.Reals.RIneq]
NPEeval [in Stdlib.setoid_ring.Field_theory]
Nplus [in Stdlib.NArith.BinNat]
Nplus_succ [in Stdlib.NArith.BinNat]
Nplus_assoc [in Stdlib.NArith.BinNat]
Nplus_comm [in Stdlib.NArith.BinNat]
Nplus_0_r [in Stdlib.NArith.BinNat]
Nplus_0_l [in Stdlib.NArith.BinNat]
Npos [in Stdlib.NArith.BinNat]
NPphi_pow [in Stdlib.setoid_ring.Field_theory]
NPphi_dev [in Stdlib.setoid_ring.Field_theory]
Npred_minus [in Stdlib.NArith.BinNat]
NProp [in Stdlib.Logic.ClassicalFacts]
Nrec [in Stdlib.NArith.BinNat]
Nrect [in Stdlib.NArith.BinNat]
Nrect_step [in Stdlib.NArith.BinNat]
Nrect_base [in Stdlib.NArith.BinNat]
Nrec_succ [in Stdlib.NArith.BinNat]
Nrec_base [in Stdlib.NArith.BinNat]
Nsqrt_spec [in Stdlib.NArith.Nsqrt_def]
Nsucc_0 [in Stdlib.NArith.BinNat]
nth_error_O [in Stdlib.Lists.List]
nth_error_cons_S [in Stdlib.Lists.List]
null [in Stdlib.micromega.Tauto]
NZCyclicAxiomsMod.P [in Stdlib.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.S [in Stdlib.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.wB [in Stdlib.Numbers.Cyclic.Abstract.NZCyclic]
NZMulOrderProp.mul_eq_0_r [in Stdlib.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_eq_0_l [in Stdlib.Numbers.NatInt.NZMulOrder]
NZMulOrderProp.mul_eq_0 [in Stdlib.Numbers.NatInt.NZMulOrder]
NZOrderProp.lt_ngt [in Stdlib.Numbers.NatInt.NZOrder]
NZOrderProp.lt_eq_gt_cases [in Stdlib.Numbers.NatInt.NZOrder]
n_of_Z [in Stdlib.micromega.ZMicromega]
N_of_Z [in Stdlib.setoid_ring.ZArithRing]
N_of_nat [in Stdlib.NArith.BinNat]
N_ind [in Stdlib.NArith.BinNat]
N_rec [in Stdlib.NArith.BinNat]
N_rect [in Stdlib.NArith.BinNat]
N_of_max [in Stdlib.NArith.Nnat]
N_of_min [in Stdlib.NArith.Nnat]
N_of_nat_pow [in Stdlib.NArith.Nnat]
N_of_nat_mod [in Stdlib.NArith.Nnat]
N_of_nat_div [in Stdlib.NArith.Nnat]
N_of_nat_compare [in Stdlib.NArith.Nnat]
N_of_div2 [in Stdlib.NArith.Nnat]
N_of_mult [in Stdlib.NArith.Nnat]
N_of_minus [in Stdlib.NArith.Nnat]
N_of_plus [in Stdlib.NArith.Nnat]
N_of_pred [in Stdlib.NArith.Nnat]
N_of_S [in Stdlib.NArith.Nnat]
N_of_double_plus_one [in Stdlib.NArith.Nnat]
N_of_double [in Stdlib.NArith.Nnat]
N_of_nat_inj [in Stdlib.NArith.Nnat]
N_of_nat_of_N [in Stdlib.NArith.Nnat]
N.pos [in Stdlib.NArith.BinNatDef]
N0 [in Stdlib.NArith.BinNat]

Global Index

(26071 entries)

Notation Index

F

J

K

T

X

Y

_

(1003 entries)

Module Index

J

X

Y

_

other

(815 entries)

Variable Index

J

Q

V

X

Y

_

other

(1771 entries)

Library Index

K

X

Y

_

other

(589 entries)

Constructor Index

K

Y

_

other

(961 entries)

Lemma Index

other

(12021 entries)

Axiom Index

J

K

V

X

Y

_

other

(508 entries)

Inductive Index

X

Y

_

other

(308 entries)

Projection Index

G

K

X

Y

_

other

(479 entries)

Section Index

J

Q

X

Y

_

other

(496 entries)

Instance Index

J

V

X

Y

_

other

(906 entries)

Abbreviation Index

J

Y

_

other

(1204 entries)

Definition Index

_

other

(4844 entries)

Record Index

J

X

Y

_

other

(166 entries)