intro h
case step
n : Nat
ih : n.isOdd = true → n.half.inr = n
⊢ (n + 2).isOdd = true → (n + 2).half.inr = n + 2
case step
n : Nat
ih : n.isOdd = true → n.half.inr = n
h : (n + 2).isOdd = true
⊢ (n + 2).half.inr = n + 2