no goals
m n : Nat
⊢ n * (m / n) ≤ m
match n, Nat.eq_zero_or_pos n with
| _, Or.inl rfl => rw [Nat.zero_mul]; exact m.zero_le
| n, Or.inr h => rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le h]; exact Nat.le_refl _
m n : Nat
⊢ 0 ≤ m
m n : Nat
⊢ 0 * (m / 0) ≤ m
rw [Nat.zero_mul]
no goals
m n : Nat
⊢ 0 ≤ m
exact m.zero_le
m n✝ n : Nat
h : n > 0
⊢ m / n ≤ m / n
m n✝ n : Nat
h : n > 0
⊢ n * (m / n) ≤ m
rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le h]
no goals
m n✝ n : Nat
h : n > 0
⊢ m / n ≤ m / n
exact Nat.le_refl _