apply Nat.add_le_add
case succ_succ.h
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m.tri + m ≤ n.tri + n
case succ_succ.h.h₁
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m.tri ≤ n.tri

case succ_succ.h.h₂
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m ≤ n