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