feat(Data/ENNReal/Inv): add div_mul_div_cancel

Proves a / b * (b / c) = a / c for b ≠ 0, b ≠ ∞ in ENNReal.
Proof via mul_div_assoc and existing div_mul_cancel.

AI Disclosure: This PR was developed with assistance from an LLM (Claude, Anthropic) for proof exploration and text drafting. The proof was compiled and verified locally by the contributor, who understands the mathematical content. This lemma is extracted from a larger formalization of information-theoretic bounds (Zenodo DOI: 10.5281/zenodo.19317983).

Author: jdhart81

Mathlib/Data/ENNReal/Inv.lean

@@ -169,6 +169,11 @@ protected lemma div_mul_cancel' (ha₀ : a = 0 → b = 0) (ha : a = ∞ → b =
 protected lemma div_mul_cancel (ha₀ : a ≠ 0) (ha : a ≠ ∞) : b / a * a = b :=
   ENNReal.div_mul_cancel' (by simp [ha₀]) (by simp [ha])
 
+/-- Cancels a shared denominator: `a / b * (b / c) = a / c` for `b ≠ 0`, `b ≠ ∞` in `ℝ≥0∞`. -/
+protected lemma div_mul_div_cancel (hb₀ : b ≠ 0) (hb : b ≠ ∞) :
+    a / b * (b / c) = a / c := by
+  rw [← mul_div_assoc, ENNReal.div_mul_cancel hb₀ hb]
+
 /-- See `ENNReal.mul_div_cancel` for a simpler version assuming `a ≠ 0`, `a ≠ ∞`. -/
 protected lemma mul_div_cancel' (ha₀ : a = 0 → b = 0) (ha : a = ∞ → b = 0) : a * (b / a) = b := by
   rw [mul_comm, ENNReal.div_mul_cancel' ha₀ ha]