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