exact lt_defn_add.mpr
  ⟨d * m, ‹Positive (d * m)›, ‹n₂ * m ≃ n₁ * m + d * m›⟩
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
x✝¹ : Positive m
x✝ : n₁ < n₂
d : ℕ
left✝ : Positive d
right✝ : n₂ ≃ n₁ + d
this✝ : n₂ * m ≃ n₁ * m + d * m
this : Positive (d * m)
⊢ n₁ * m < n₂ * m
no goals