Theorem: Nat.mod_two_ne_zero (Smt/Reconstruct/Int/Lemmas.lean)

State before:
n : Nat
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
Tactic:
cases Nat.mod_two_eq_zero_or_one n <;> rename_i h <;> simp [h]
State after:
no goals