rw [tri_succ, tri_succ]
case succ_succ
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ (m + 1).tri ≤ (n + 1).tri
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