Theoremscast_ofZNum, cast_sub', div_to_nat, div_zero, dvd_iff_mod_eq_zero, gcd_to_nat, gcd_to_nat_aux, mem_ofZNum', mod_to_nat, mod_zero, ofInt'_toZNum, ofZNum'_toNat, ofZNum_toNat, pred_succ, sub_to_nat, succ_ofInt', toZNumNeg_succ, toZNum_succ, cast_sub', cast_to_znum, div'_to_nat, divMod_to_nat, divMod_to_nat_aux, mod'_to_nat, to_int_eq_succ_pred, to_nat_eq_succ_pred, abs_toZNum, abs_to_nat, add_one, add_zero, bit0_of_bit0, bit1_of_bit1, cast_add, cast_bit0, cast_bit1, cast_bitm1, cast_inj, cast_le, cast_lt, cast_mul, cast_neg, cast_one, cast_pos, cast_sub, cast_succ, cast_to_int, cast_zero, cast_zero', cast_zneg, cmp_to_int, div_to_int, div_zero, dvd_iff_mod_eq_zero, dvd_to_int, gcd_to_nat, isOrderedAddMonoid, isStrictOrderedRing, le_to_int, lt_to_int, mod_to_int, mul_to_int, neg_of_int, neg_zero, nontrivial, ofInt'_eq, ofInt'_neg, of_intCast, of_natCast, of_nat_toZNum, of_nat_toZNumNeg, of_to_int, of_to_int', to_int_inj, to_of_int, zeroLEOneClass, zero_add, zneg_bit1, zneg_bitm1, zneg_neg, zneg_pos, zneg_pred, zneg_succ, zneg_zneg | 83 |