Theorem: Misc.Nat.odd_succ_of_even (LeanSAT/Util/Misc.lean)

State before:
n : Nat
⊢ Even n → Odd n.succ
Tactic:
intro ⟨r, hr⟩
State after:
n r : Nat
hr : n = r + r
⊢ Odd n.succ

State before:
n r : Nat
hr : n = r + r
⊢ Odd n.succ
Tactic:
exists r
State after:
n r : Nat
hr : n = r + r
⊢ n.succ = 2 * r + 1

State before:
n r : Nat
hr : n = r + r
⊢ n.succ = 2 * r + 1
Tactic:
simp_arith [hr]
State after:
no goals