diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean
index f85079ea9cb3c6..98d40b50e16f68 100644
--- a/Mathlib/Data/Nat/Basic.lean
+++ b/Mathlib/Data/Nat/Basic.lean
@@ -707,6 +707,26 @@ protected theorem div_left_inj {a b d : ℕ} (hda : d ∣ a) (hdb : d ∣ b) : a
   rw [← Nat.mul_div_cancel' hda, ← Nat.mul_div_cancel' hdb, h]
 #align nat.div_left_inj Nat.div_left_inj
 
+theorem div_mul_div_comm {l : ℕ} (hmn : n ∣ m) (hkl : l ∣ k) :
+    (m / n) * (k / l) = (m * k) / (n * l) := by
+  obtain ⟨x, rfl⟩ := hmn
+  obtain ⟨y, rfl⟩ := hkl
+  rcases n.eq_zero_or_pos with rfl | hn
+  · simp
+  rcases l.eq_zero_or_pos with rfl | hl
+  · simp
+  rw [Nat.mul_div_cancel_left _ hn, Nat.mul_div_cancel_left _ hl, mul_assoc n, Nat.mul_left_comm x,
+    ←mul_assoc n, Nat.mul_div_cancel_left _ (Nat.mul_pos hn hl)]
+#align nat.div_mul_div_comm Nat.div_mul_div_comm
+
+protected theorem div_pow {a b c : ℕ} (h : a ∣ b) : (b / a) ^ c = b ^ c / a ^ c := by
+  rcases c.eq_zero_or_pos with rfl | hc
+  · simp
+  rcases a.eq_zero_or_pos with rfl | ha
+  · simp [Nat.zero_pow hc]
+  refine (Nat.div_eq_of_eq_mul_right (pos_pow_of_pos c ha) ?_).symm
+  rw [←Nat.mul_pow, Nat.mul_div_cancel_left' h]
+
 /-! ### `mod`, `dvd` -/
 
 
diff --git a/Mathlib/Data/Nat/Order/Basic.lean b/Mathlib/Data/Nat/Order/Basic.lean
index ea58274bb664bd..2d108d231bc391 100644
--- a/Mathlib/Data/Nat/Order/Basic.lean
+++ b/Mathlib/Data/Nat/Order/Basic.lean
@@ -506,26 +506,6 @@ theorem add_mod_eq_ite :
   · exact Nat.mod_eq_of_lt (lt_of_not_ge h)
 #align nat.add_mod_eq_ite Nat.add_mod_eq_ite
 
-theorem div_mul_div_comm (hmn : n ∣ m) (hkl : l ∣ k) : m / n * (k / l) = m * k / (n * l) :=
-  have exi1 : ∃ x, m = n * x := hmn
-  have exi2 : ∃ y, k = l * y := hkl
-  if hn : n = 0 then by simp [hn]
-  else
-    have : 0 < n := Nat.pos_of_ne_zero hn
-    if hl : l = 0 then by simp [hl]
-    else by
-      have : 0 < l := Nat.pos_of_ne_zero hl
-      cases' exi1 with x hx
-      cases' exi2 with y hy
-      rw [hx, hy, Nat.mul_div_cancel_left, Nat.mul_div_cancel_left]
-      apply Eq.symm
-      apply Nat.div_eq_of_eq_mul_left
-      apply mul_pos
-      repeat' assumption
-      -- Porting note: this line was `cc` in Lean3
-      simp only [mul_comm, mul_left_comm, mul_assoc]
-#align nat.div_mul_div_comm Nat.div_mul_div_comm
-
 theorem div_eq_self : m / n = m ↔ m = 0 ∨ n = 1 := by
   constructor
   · intro