simp only [split]
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ (n + 1).split.fst.tri + ↑(n + 1).split.snd = n.split.fst.tri + (↑n.split.snd + 1)
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
⊢ (if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).fst.tri +
      ↑(if h : ↑n.split.2 < n.split.fst then ⟨n.split.fst, ⟨↑n.split.2 + 1, ⋯⟩⟩ else ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩).snd =
    n.split.fst.tri + (↑n.split.snd + 1)