Theorem: ipow_lt_zero (HOLFloat/Common.lean)

State before:
r : ℝ
i : ℤ
⊢ 0 < r → 0 < r ^ i
Tactic:
intro h
State after:
r : ℝ
i : ℤ
h : 0 < r
⊢ 0 < r ^ i

State before:
r : ℝ
i : ℤ
h : 0 < r
⊢ 0 < r ^ i
Tactic:
cases i with 
| ofNat n  =>
  simp_all only [Int.ofNat_eq_coe, zpow_coe_nat, gt_iff_lt, pow_pos]
| negSucc n =>
  simp_all only [zpow_negSucc, inv_pos, gt_iff_lt, pow_pos]
State after:
no goals

State before:
case ofNat
r : ℝ
h : 0 < r
n : ℕ
⊢ 0 < r ^ ofNat n
Tactic:
simp_all only [Int.ofNat_eq_coe, zpow_coe_nat, gt_iff_lt, pow_pos]
State after:
no goals

State before:
case negSucc
r : ℝ
h : 0 < r
n : ℕ
⊢ 0 < r ^ -[n+1]
Tactic:
simp_all only [zpow_negSucc, inv_pos, gt_iff_lt, pow_pos]
State after:
no goals