Theoremsadd_ofNat', add_of_nat, add_one, add_succ, add_toZNum, add_to_nat, add_zero, bit0_of_bit0, bit1_of_bit1, bit1_succ, bit_to_nat, castNum_and, castNum_eq_bitwise, castNum_ldiff, castNum_or, castNum_shiftLeft, castNum_shiftRight, castNum_testBit, castNum_xor, cast_add, cast_bit0, cast_bit1, cast_inj, cast_le, cast_lt, cast_mul, cast_one, cast_pos, cast_succ, cast_succ', cast_toZNum, cast_toZNumNeg, cast_to_int, cast_to_nat, cast_zero, cast_zero', cmp_eq, cmp_swap, cmp_to_nat, dvd_to_nat, isOrderedCancelAddMonoid, isStrictOrderedRing, le_iff_cmp, le_to_nat, lt_iff_cmp, lt_to_nat, mul_to_nat, natSize_to_nat, ofNat'_bit, ofNat'_eq, ofNat'_one, ofNat'_succ, ofNat'_zero, of_natCast, of_nat_inj, of_to_nat, of_to_nat', ppred_to_nat, pred_to_nat, size_eq_natSize, size_to_nat, succ'_to_nat, succ_to_nat, toNat_injective, toZNum_inj, to_nat_inj, to_nat_to_int, to_of_nat, zero_add, zneg_toZNum, zneg_toZNumNeg, add_one, add_succ, add_to_nat, bit0_of_bit0, bit1_of_bit1, bit_to_nat, cast_add, cast_bit0, cast_bit1, cast_inj, cast_le, cast_lt, cast_mul, cast_one, cast_one', cast_pos, cast_succ, cast_to_int, cast_to_nat, cast_to_num, cmp_eq, cmp_swap, cmp_to_nat, cmp_to_nat_lemma, dvd_to_nat, le_iff_cmp, le_to_nat, lt_iff_cmp, lt_to_nat, mul_to_nat, natSize_pos, natSize_to_nat, of_to_nat, of_to_nat', one_add, one_le_cast, one_sub', pred'_succ', pred'_to_nat, pred_to_nat, size_eq_natSize, size_to_nat, sub'_one, succ'_pred', succ_to_nat, to_nat_inj, to_nat_pos, to_nat_to_int | 119 |