induction n using Nat.recTwo with
| zero => intro; contradiction
| one => intro; rfl
| step n ih =>
  intro h
  unfold Nat.inr at ih ⊢
  unfold Nat.half
  rw [Nat.mul_succ, Nat.add_succ, Nat.add_succ, ih h]
n : Nat
⊢ n.isOdd = true → n.half.inr = n
no goals