BKLNW.rpow_le_of_pow_le

lemma rpow_le_of_pow_le {a c : ℝ} (ha : 0 ≤ a) (hc : 0 ≤ c) {p q : ℕ} (hq : q ≠ 0)    (h : a ^ p ≤ c ^ q) : a ^ (p / (q : ℝ)) ≤ c := by  have hpow : (a ^ (p / (q : ℝ))) ^ q = a ^ p := by    have hq' : (q : ℝ) ≠ 0 := by exact_mod_cast hq    calc      (a ^ (p / (q : ℝ))) ^ q = a ^ ((p / (q : ℝ)) * q) := by        symm        exact Real.rpow_mul_natCast ha (p / (q : ℝ)) q      _ = a ^ (p : ℝ) := by        field_simp [hq']      _ = a ^ p := by        simp [Real.rpow_natCast]  have h' : (a ^ (p / (q : ℝ))) ^ q ≤ c ^ q := by    simpa [hpow] using h  exact (pow_le_pow_iff_left₀ (by positivity) hc hq).1 h'