Theoremsadd_one_le_of_lt, castLE_natCast, castLT_sub_nezero, cast_eq_self, cast_eq_zero, cast_injective, cast_val_eq_self, coe_int_add_eq_ite, coe_int_add_eq_mod, coe_int_sub_eq_ite, coe_int_sub_eq_mod, coe_natCast_eq_mod, coe_neg_one, coe_ofNat_eq_mod, default_eq_zero, eq_one_of_ne_zero, eq_zero, equivSubtype_apply, equivSubtype_symm_apply, exists_eq_add_of_le, exists_eq_add_of_lt, exists_ne_and_ne_of_two_lt, heq_ext_iff, heq_fun_iff, heq_fun₂_iff, instCanLiftNatValLt, instNeZeroHAddNatOfNat_mathlib, instNontrivial, intCast_val_sub_eq_sub_add_ite, last_pos', last_sub, le_iff_val_le_val, le_or_gt, le_val_last, liftFun_iff_succ, lt_last_iff_ne_last, lt_or_ge, max_val, min_val, mk_eq_mk, mk_eq_one, mk_zero', modNat_rev, mul_one', mul_zero', natCast_eq_last, natCast_eq_mk, natCast_eq_zero, natCast_le_natCast, natCast_lt_natCast, natCast_mono, natCast_self, natCast_strictMono, natCast_zero, neZero, ne_iff_vne, ne_last_of_lt, ne_zero_of_lt, nontrivial_iff_two_le, ofNat_eq_cast, one_eq_mk, one_eq_mk_of_lt, one_le_of_ne_zero, one_lt_last, one_mul', pos_iff_ne_zero', pos_of_ne_zero, prop, size_positive, size_positive', sub_succ_le_sub_of_le, sub_val_lt_sub, val_add_eq_ite, val_add_eq_of_add_lt, val_add_one_of_lt', val_cast_of_lt, val_eq_val, val_fin_le, val_fin_lt, val_injective, val_natCast, val_one', val_pos_iff, val_sub_one_of_ne_zero, zero_mul', exists_lt_iff_fin, forall_lt_iff_fin | 87 |