transitivity (tri (split (pair x y)).fst + (split (pair x y)).snd)
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ t.tri + s = (x + y).tri + x
case left
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ t.tri + s = (x.pair y).split.fst.tri + ↑(x.pair y).split.snd

case right
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ (x.pair y).split.fst.tri + ↑(x.pair y).split.snd = (x + y).tri + x