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

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

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

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