apply Nat.tri_add_inj (Nat.le_of_lt_succ hs) (Nat.le_add_right x y)
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ ⟨t, ⟨s, hs⟩⟩.fst = x + y
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ t.tri + s = (x + y).tri + x