m n k l : ℕ
h : 0 < n
⊢ m * 1 ≤ m * n
m n k l : ℕ
h : 0 < n
⊢ m ≤ m * n
conv =>
  lhs
  rw [← mul_one m]
no goals
m n k l : ℕ
h : 0 < n
⊢ m * 1 ≤ m * n
exact mul_le_mul_of_nonneg_left h.nat_succ_le (zero_le _)