unfold Nat.half
case step
n : Nat
ih : n.isOdd = true → 2 * n.half + 1 = n
h : (n + 2).isOdd = true
⊢ 2 * (n + 2).half + 1 = n + 2
case step
n : Nat
ih : n.isOdd = true → 2 * n.half + 1 = n
h : (n + 2).isOdd = true
⊢ 2 * (n.half + 1) + 1 = n + 2