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 (18816 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 (644 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 (708 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 (1456 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 (407 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 (8932 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 (422 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 (699 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 (209 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 (203 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 (550 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 (338 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 (1235 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 (2946 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 (67 entries)

N (abbreviation)

nat_of_Nplus [in nat_of_Nplus]
nat_of_P_inj_iff [in nat_of_P_inj_iff]
nat_of_P_of_succ_nat [in nat_of_P_of_succ_nat]
nat_of_P_o_P_of_succ_nat_eq_succ [in nat_of_P_o_P_of_succ_nat_eq_succ]
nat_of_P_is_S [in nat_of_P_is_S]
nat_of_P_mult_morphism [in nat_of_P_mult_morphism]
nat_of_P_plus_morphism [in nat_of_P_plus_morphism]
nat_of_Ndiv2 [in nat_of_Ndiv2]
nat_of_P_xI [in nat_of_P_xI]
nat_of_P [in nat_of_P]
nat_of_P_xH [in nat_of_P_xH]
nat_of_Ndouble_plus_one [in nat_of_Ndouble_plus_one]
nat_of_P_succ_morphism [in nat_of_P_succ_morphism]
nat_of_N_of_nat [in nat_of_N_of_nat]
nat_of_P_xO [in nat_of_P_xO]
nat_of_Nmax [in nat_of_Nmax]
nat_of_N [in nat_of_N]
nat_of_Ncompare [in nat_of_Ncompare]
nat_of_Nmin [in nat_of_Nmin]
nat_of_Nsucc [in nat_of_Nsucc]
nat_of_Ndouble [in nat_of_Ndouble]
nat_of_P_pos [in nat_of_P_pos]
nat_of_P_inj [in nat_of_P_inj]
nat_of_N_inj [in nat_of_N_inj]
nat_of_Nminus [in nat_of_Nminus]
nat_of_Npred [in nat_of_Npred]
nat_of_P_compare_morphism [in nat_of_P_compare_morphism]
nat_of_Nmult [in nat_of_Nmult]
Nbit [in Nbit]
NBitsProp.lnextcarry [in lnextcarry]
NBitsProp.lxor3 [in lxor3]
NBitsProp.nextcarry [in nextcarry]
NBitsProp.xor3 [in xor3]
Nbit0 [in Nbit0]
Ncompare [in Ncompare]
Ncompare_refl [in Ncompare_refl]
Ncompare_eq_correct [in Ncompare_eq_correct]
Ncompare_spec [in Ncompare_spec]
Ncompare_0 [in Ncompare_0]
Ncompare_Eq_eq [in Ncompare_Eq_eq]
Ndiscr [in Ndiscr]
Ndiv [in Ndiv]
Ndivide [in Ndivide]
Ndiv_Zquot [in Ndiv_Zquot]
Ndiv_mod_eq [in Ndiv_mod_eq]
Ndiv_eucl [in Ndiv_eucl]
Ndiv_eucl_correct [in Ndiv_eucl_correct]
Ndiv2 [in Ndiv2]
Ndouble [in Ndouble]
Ndouble_plus_one_div2 [in Ndouble_plus_one_div2]
Ndouble_inj [in Ndouble_inj]
Ndouble_div2 [in Ndouble_div2]
Ndouble_plus_one [in Ndouble_plus_one]
Ndouble_plus_one_inj [in Ndouble_plus_one_inj]
negb_intro [in negb_intro]
negb_elim [in negb_elim]
Neqb [in Neqb]
Neqb [in Neqb]
Neqb_eq [in Neqb_eq]
Neqb_comm [in Neqb_comm]
Neqb_correct [in Neqb_correct]
neq_O_lt [in neq_O_lt]
Neven [in Neven]
Neven_spec [in Neven_spec]
Ngcd [in Ngcd]
Ngcd_divide_r [in Ngcd_divide_r]
Ngcd_greatest [in Ngcd_greatest]
Ngcd_divide_l [in Ngcd_divide_l]
Nge [in Nge]
Nggcd [in Nggcd]
Nggcd_correct_divisors [in Nggcd_correct_divisors]
Nggcd_gcd [in Nggcd_gcd]
Ngt [in Ngt]
Ngt_Nlt [in Ngt_Nlt]
Nil [in Nil]
nil [in nil]
nil_sort [in nil_sort]
nil_leA [in nil_leA]
Nind [in Nind]
Nle [in Nle]
Nle_succ_l [in Nle_succ_l]
Nle_trans [in Nle_trans]
Nle_0 [in Nle_0]
Nle_lteq [in Nle_lteq]
Nlog2 [in Nlog2]
Nlog2_spec [in Nlog2_spec]
Nlog2_nonpos [in Nlog2_nonpos]
Nlt [in Nlt]
Nlt_irrefl [in Nlt_irrefl]
Nlt_not_eq [in Nlt_not_eq]
Nlt_trans [in Nlt_trans]
Nlt_succ_r [in Nlt_succ_r]
Nmax [in Nmax]
Nmin [in Nmin]
Nminus [in Nminus]
Nminus_N0_Nle [in Nminus_N0_Nle]
Nminus_succ_r [in Nminus_succ_r]
Nminus_0_r [in Nminus_0_r]
Nmin_choice [in Nmin_choice]
Nmod [in Nmod]
Nmod_lt [in Nmod_lt]
Nmod_Zrem [in Nmod_Zrem]
NMulOrderProp.mul_pos [in mul_pos]
Nmult [in Nmult]
Nmult_plus_distr_r [in Nmult_plus_distr_r]
Nmult_comm [in Nmult_comm]
Nmult_0_l [in Nmult_0_l]
Nmult_1_l [in Nmult_1_l]
Nmult_assoc [in Nmult_assoc]
Nmult_1_r [in Nmult_1_r]
Nodd [in Nodd]
Nodd_spec [in Nodd_spec]
not_O_IZR [in not_O_IZR]
not_nm_INR [in not_nm_INR]
not_INR_O [in not_INR_O]
not_eq_sym [in not_eq_sym]
not_O_INR [in not_O_INR]
Nplus [in Nplus]
Nplus_comm [in Nplus_comm]
Nplus_0_l [in Nplus_0_l]
Nplus_assoc [in Nplus_assoc]
Nplus_succ [in Nplus_succ]
Nplus_0_r [in Nplus_0_r]
Npos [in Npos]
Npow [in Npow]
Npow_succ_r [in Npow_succ_r]
Npow_0_r [in Npow_0_r]
Npred [in Npred]
Npred_succ [in Npred_succ]
Npred_minus [in Npred_minus]
Nrec [in Nrec]
Nrect [in Nrect]
Nrect_step [in Nrect_step]
Nrect_base [in Nrect_base]
Nrec_base [in Nrec_base]
Nrec_succ [in Nrec_succ]
Nsize [in Nsize]
Nsqrt [in Nsqrt]
Nsqrtrem [in Nsqrtrem]
Nsqrtrem_spec [in Nsqrtrem_spec]
Nsqrtrem_sqrt [in Nsqrtrem_sqrt]
Nsqrt_spec [in Nsqrt_spec]
Nsucc [in Nsucc]
Nsucc_pos_spec [in Nsucc_pos_spec]
Nsucc_0 [in Nsucc_0]
Nsucc_pred [in Nsucc_pred]
Nsucc_inj [in Nsucc_inj]
Nsucc_pos [in Nsucc_pos]
Nxor [in Nxor]
Nxor_neutral_right [in Nxor_neutral_right]
Nxor_assoc [in Nxor_assoc]
Nxor_comm [in Nxor_comm]
Nxor_eq [in Nxor_eq]
Nxor_nilpotent [in Nxor_nilpotent]
Nxor_neutral_left [in Nxor_neutral_left]
NZCyclicAxiomsMod.P [in P]
NZCyclicAxiomsMod.S [in S]
NZCyclicAxiomsMod.wB [in wB]
NZOrderProp.lt_ngt [in lt_ngt]
NZOrderProp.lt_eq_gt_cases [in lt_eq_gt_cases]
N_of_nat_of_N [in N_of_nat_of_N]
N_of_div2 [in N_of_div2]
N_of_pred [in N_of_pred]
N_ind [in N_ind]
N_rect [in N_rect]
N_of_nat_compare [in N_of_nat_compare]
N_of_minus [in N_of_minus]
N_of_min [in N_of_min]
N_of_plus [in N_of_plus]
N_eq_dec [in N_eq_dec]
N_of_double [in N_of_double]
N_of_nat [in N_of_nat]
N_of_max [in N_of_max]
N_of_mult [in N_of_mult]
N_of_S [in N_of_S]
N_of_double_plus_one [in N_of_double_plus_one]
N_of_nat_inj [in N_of_nat_inj]
N_rec [in N_rec]
N.pos [in pos]
N0 [in N0]



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 (18816 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 (644 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 (708 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 (1456 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 (407 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 (8932 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 (422 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 (699 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 (209 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 (203 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 (550 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 (338 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 (1235 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 (2946 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 (67 entries)