apply Nat.add_le_add_right
case succ_succ
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m.tri + m + 1 ≤ n.tri + n + 1
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