a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
H1 : 0 ≤ b
H2 : b ∣ a
H3 : a / b ≤ c
⊢ a / b * b ≤ c * b
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
H1 : 0 ≤ b
H2 : b ∣ a
H3 : a / b ≤ c
⊢ a ≤ c * b
rw [← Int.ediv_mul_cancel H2]
no goals
a✝ b✝ : ℤ
n : ℕ
a b c : ℤ
H1 : 0 ≤ b
H2 : b ∣ a
H3 : a / b ≤ c
⊢ a / b * b ≤ c * b
exact mul_le_mul_of_nonneg_right H3 H1