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

State before:
n : Nat
⊢ (n + 1) % 2 = 0 ↔ n % 2 ≠ 0
Tactic:
simp [Nat.even_add]
State after:
no goals