case h.e'_4
x✝ y z✝ x z : ℝ
hx : 1 ≤ x
hz : z ≤ 0
⊢ 1 = x ^ 0
x✝ y z✝ x z : ℝ
hx : 1 ≤ x
hz : z ≤ 0
⊢ x ^ z ≤ 1
convert rpow_le_rpow_of_exponent_le hx hz
no goals
case h.e'_4
x✝ y z✝ x z : ℝ
hx : 1 ≤ x
hz : z ≤ 0
⊢ 1 = x ^ 0
exact (rpow_zero x).symm