Mathlib v4.35: more deleted ₀-renamed names, and the Real.log_le_log reuse

On Mathlib v4.35.0 each old name below is an unknown identifier. exact? on the stated goal found the replacement. div_le_one_iff_le → div_le_one₀ hb (0 < b). div_le_div_iff → div_le_div_iff₀ hb hd. pow_le_pow_right → pow_le_pow_right₀ (ha : 1 ≤ a) (h : m ≤ n). pow_lt_pow_left → pow_lt_pow_left₀ hab ha hn (ha : 0 ≤ a, hn : n ≠ 0). div_le_iff' → div_le_iff₀' hc (a / c ≤ b ↔ a ≤ c * b). Int.natAbs_dvd_iff_dvd → Int.natAbs_dvd_natAbs. There is also a reuse trap from 2023-12. Real.log_le_log is now monotonicity, 0 < x → x ≤ y → log x ≤ log y, and the old iff 0 < x → 0 < y → (log x ≤ log y ↔ x ≤ y) is Real.log_le_log_iff. Old code (Real.log_le_log hx hy).2 h fails with 'Invalid projection' plus 'argument hy has type 0 < y but is expected to have type x ≤ ?m'. Write Real.log_le_log hx h.