TheoremsnnratCast_eq, nnratCast_le, nnratCast_lt, nnratCast_ne, abs_coe, add_def, bddAbove_coe, bddBelow_coe, canLift, coe_add, coe_coeHom, coe_divNat, coe_eq_zero, coe_inj, coe_injective, coe_le_coe, coe_lt_coe, coe_max, coe_min, coe_mk, coe_mono, coe_mul, coe_natCast, coe_ne_zero, coe_nonneg, coe_one, coe_pos, coe_pow, coe_sub, coe_zero, coprime_num_den, den_coe, den_mul_eq_num, den_natCast, den_ne_zero, den_ofNat, den_one, den_pos, den_pow, den_zero, divNat_inj, divNat_mul_divNat, divNat_mul_left, divNat_mul_right, divNat_zero, exists, ext, ext_iff, ext_num_den, ext_num_den_iff, forall, instCharZero, instNontrivial, le_def, lt_def, mk_divInt, mk_natCast, mk_zero, mul_def, mul_den_eq_num, natAbs_num_coe, natCast_eq_divNat, ne_iff, nonpos_iff_eq_zero, nsmul_coe, num_coe, num_divNat_den, num_natCast, num_ne_zero, num_ofNat, num_one, num_pos, num_pow, num_zero, sub_def, toNNRat_coe, toNNRat_coe_nat, toNNRat_mono, val_eq_cast, coe_nnabs, coe_toNNRat, instPosMulMono, le_coe_toNNRat, le_toNNRat_iff_coe_le, le_toNNRat_iff_coe_le', lt_toNNRat_iff_coe_lt, toNNRat_add, toNNRat_add_le, toNNRat_eq_zero, toNNRat_le_iff_le_coe, toNNRat_le_toNNRat_iff, toNNRat_lt_iff_lt_coe, toNNRat_lt_toNNRat_iff, toNNRat_lt_toNNRat_iff', toNNRat_lt_toNNRat_iff_of_nonneg, toNNRat_mul, toNNRat_of_nonpos, toNNRat_one, toNNRat_pos, toNNRat_zero | 100 |