Theorem: odd_succ_even (LeanCourse/Extra.lean)

State before:
n : ℕ
h : EvenNat n
⊢ OddNat (n + 1)
Tactic:
refine Even.add_odd h ?_
State after:
n : ℕ
h : EvenNat n
⊢ Odd 1

State before:
n : ℕ
h : EvenNat n
⊢ Odd 1
Tactic:
norm_num
State after:
no goals