apply Nat.add_le_add_left
case h.left
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁.tri + m₁ ≤ n₁.tri + n₁
case h.left.h
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ m₁ ≤ n₁