have : n₁ + m ≄ n₂ + m := mt AA.cancelR ‹n₁ ≄ n₂›
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
left✝ : n₁ ≤ n₂
right✝ : n₁ ≄ n₂
this : n₁ + m ≤ n₂ + m
⊢ n₁ + m < n₂ + m
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
left✝ : n₁ ≤ n₂
right✝ : n₁ ≄ n₂
this✝ : n₁ + m ≤ n₂ + m
this : n₁ + m ≄ n₂ + m
⊢ n₁ + m < n₂ + m