m n k a b c : ℕ
H : 0 < b
H' : b ∣ a
⊢ a / b = c ↔ a = b * c
m n k a b c : ℕ
H : 0 < b
H' : b ∣ a
⊢ a / b = c ↔ a = c * b
rw [mul_comm]
no goals
m n k a b c : ℕ
H : 0 < b
H' : b ∣ a
⊢ a / b = c ↔ a = b * c
exact Nat.div_eq_iff_eq_mul_right H H'