no goals
a✝ b✝ m n k a b c : ℕ
h : a * b ∣ c
ha : a = 0
⊢ b ∣ c / a
simp [ha]
no goals
a✝ b✝ m n k a b c : ℕ
h : a * b ∣ c
ha✝ : ¬a = 0
ha : 0 < a
h1 : ∃ d, c = a * b * d
d : ℕ
hd : c = a * b * d
⊢ c = a * (b * d)
simpa [mul_assoc] using hd