unfold Nat.inr at ih ⊢
case step
n : Nat
ih : n.isOdd = true → n.half.inr = n
h : (n + 2).isOdd = true
⊢ (n + 2).half.inr = n + 2
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