feat(algebra/euclidean_domain,data/int/basic): dvd_div_of_mul_dvd (#12382)

We have a separate `int` and `euclidean_domain` version as `euclidean_domain` isn't pulled in by `int.basic`.

Author: ericrbg

src/algebra/euclidean_domain.lean

@@ -195,6 +195,15 @@ begin
       euclidean_domain.mul_div_cancel _ hq]
 end
 
+lemma dvd_div_of_mul_dvd {a b c : R} (h : a * b ∣ c) : b ∣ c / a :=
+begin
+  rcases eq_or_ne a 0 with rfl | ha,
+  { simp only [div_zero, dvd_zero] },
+  rcases h with ⟨d, rfl⟩,
+  refine ⟨d, _⟩,
+  rw [mul_assoc, mul_div_cancel_left _ ha]
+end
+
 section
 open_locale classical
 

src/data/int/basic.lean

@@ -1110,14 +1110,23 @@ not_lt.mp (mt (eq_zero_of_dvd_of_nat_abs_lt_nat_abs hst) ht)
 lemma nat_abs_eq_of_dvd_dvd {s t : ℤ} (hst : s ∣ t) (hts : t ∣ s) : nat_abs s = nat_abs t :=
 nat.dvd_antisymm (nat_abs_dvd_iff_dvd.mpr hst) (nat_abs_dvd_iff_dvd.mpr hts)
 
-lemma div_dvd_of_ne_zero_dvd {s t : ℤ} (hst : s ∣ t) : (t / s) ∣ t :=
+lemma div_dvd_of_dvd {s t : ℤ} (hst : s ∣ t) : (t / s) ∣ t :=
 begin
-  by_cases hs : s = 0,
-  { simp [*] at *, },
+  rcases eq_or_ne s 0 with rfl | hs,
+  { simpa using hst },
   rcases hst with ⟨c, hc⟩,
   simp [hc, int.mul_div_cancel_left _ hs],
 end
 
+lemma dvd_div_of_mul_dvd {a b c : ℤ} (h : a * b ∣ c) : b ∣ c / a :=
+begin
+  rcases eq_or_ne a 0 with rfl | ha,
+  { simp only [int.div_zero, dvd_zero] },
+  rcases h with ⟨d, rfl⟩,
+  refine ⟨d, _⟩,
+  rw [mul_assoc, int.mul_div_cancel_left _ ha],
+end
+
 /-! ### to_nat -/
 
 theorem to_nat_eq_max : ∀ (a : ℤ), (to_nat a : ℤ) = max a 0