TheoremsnatAbs, of_mul_left, of_mul_right, add_one_ediv_two_mul_two_of_odd, coe_nat_two_pow_pred, ediv_two_mul_two_add_one_of_odd, even_add', even_mul_pred_self, even_mul_succ_self, even_or_odd, even_or_odd', even_sign_iff, even_sub', even_xor'_odd, even_xor'_odd', four_dvd_add_or_sub_of_odd, isSquare_natCast_iff, isSquare_ofNat_iff, natAbs_even, natAbs_odd, natCast_pow_pred, ne_of_odd_add, not_even_iff_odd, not_even_two_mul_add_one, not_odd_iff, not_odd_iff_even, not_odd_zero, odd_add, odd_add', odd_coe_nat, odd_iff, odd_mul, odd_pow, odd_pow', odd_sign_iff, odd_sub, odd_sub', two_dvd_mul_add_one, two_mul_ediv_two_add_one_of_odd, two_mul_ediv_two_of_odd, natAbs | 41 |