Theoremsadd_den_dvd, add_den_dvd_lcm, add_intCast_den, add_natCast_den, add_num_den, add_num_den', add_ofNat_den, coe_pnatDen, den_div_eq_of_coprime, den_div_intCast_eq_one_iff, den_div_natCast_eq_one_iff, den_dvd, den_inv_of_ne_zero, den_mk, den_mul_den_eq_den_mul_gcd, div_int_inj, exists, exists_eq_mul_div_num_and_eq_mul_div_den, forall, intCast_add_den, intCast_div, intCast_div_self, intCast_sub_den, inv_intCast_den, inv_intCast_den_of_pos, inv_intCast_num, inv_intCast_num_of_pos, inv_natCast_den, inv_natCast_den_of_pos, inv_natCast_num, inv_natCast_num_of_pos, inv_neg, inv_ofNat_den, inv_ofNat_num, isSquare_iff, isSquare_intCast_iff, isSquare_natCast_iff, isSquare_ofNat_iff, mkRat_add_mkRat_of_den, mul_den, mul_den_dvd, mul_num, mul_num_den', mul_self_den, mul_self_num, natCast_add_den, natCast_div, natCast_div_self, natCast_sub_den, num_den_mk, num_div_eq_of_coprime, num_dvd, num_mk, num_mul_num_eq_num_mul_gcd, ofNat_add_den, ofNat_sub_den, pnatDen_eq_iff_den_eq, pnatDen_one, pnatDen_zero, sub_den_dvd, sub_den_dvd_lcm, sub_intCast_den, sub_natCast_den, sub_ofNat_den, substr_num_den' | 65 |