m n k l : ℕ
hn : 2 ≤ n
h : m ≤ m / n
⊢ m * n ≤ m
m n k l : ℕ
hn : 2 ≤ n
h : m ≤ m / n
⊢ n * m ≤ m
rw [mul_comm]
no goals
m n k l : ℕ
hn : 2 ≤ n
h : m ≤ m / n
⊢ m * n ≤ m
exact (Nat.le_div_iff_mul_le' (lt_of_lt_of_le (by decide) hn)).1 h
no goals
m n k l : ℕ
hn : 2 ≤ n
h : m ≤ m / n
⊢ 0 < 2
decide