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