apply Nat.le_antisymm
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
⊢ ↑n.split.snd = n.split.fst
case h₁
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
⊢ ↑n.split.snd ≤ n.split.fst

case h₂
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
⊢ n.split.fst ≤ ↑n.split.snd