rw [dif_neg h, ←Nat.add_assoc, heq]
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
heq : ↑n.split.snd = n.split.fst
⊢ ⟨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)
n : Nat
H : n.split.fst.tri + ↑n.split.snd = n
h✝ : ¬↑n.split.2 < n.split.fst
h : ¬↑n.split.snd < n.split.fst
heq : ↑n.split.snd = n.split.fst
⊢ ⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.fst.tri + ↑⟨n.split.fst + 1, ⟨0, ⋯⟩⟩.snd = n.split.fst.tri + n.split.fst + 1