Extended Non-Negative Reals

Auxiliary lemmas about ℝ≥0∞.

theorem ENNReal.div_div_div_cancel_left {a b c : ENNReal} (ha : a ≠ 0) (ha' : a ≠ ⊤) (hc : c ≠ ⊤) : a / b / (a / c) = c / b