Theorem: ipow_monotone_le_pow (HOLFloat/Common.lean)

State before:
r : ℝ
u v : ℤ
⊢ 1 < r → r ^ u ≤ r ^ v → u ≤ v
Tactic:
intro a a_1
State after:
r : ℝ
u v : ℤ
a : 1 < r
a_1 : r ^ u ≤ r ^ v
⊢ u ≤ v

State before:
r : ℝ
u v : ℤ
a : 1 < r
a_1 : r ^ u ≤ r ^ v
⊢ u ≤ v
Tactic:
simp_all only [ne_eq, gt_iff_lt, zpow_le_iff_le]
State after:
no goals