match h : split n with
| ⟨t,⟨s,hs⟩⟩ =>
  rw [Nat.add_comm s, Nat.sub_add_cancel (Nat.le_of_lt_succ hs)]
  rw [←split_eq n, h]
n : Nat
⊢ (↑n.split.snd + (n.split.fst - ↑n.split.snd)).tri + ↑n.split.snd = n
no goals