Theorem: ipow_monotone_pow (HOLFloat/Common.lean)

State before:
r : ℝ
u v : ℤ
⊢ 1 ≤ r → r ^ u ≤ r ^ v → u ≤ v
Tactic:
sorry
State after:
no goals