no goals
β : Type ?u.224581
A : Type ?u.224584
G : Type ?u.224587
M : Type ?u.224590
R : Type u_1
inst✝ : StrictOrderedSemiring R
a x y : R
n m : ℕ
h : x < y
hx : 0 ≤ x
hn : 0 < 0
⊢ x ^ 0 < y ^ 0
contradiction
no goals
β : Type ?u.224581
A : Type ?u.224584
G : Type ?u.224587
M : Type ?u.224590
R : Type u_1
inst✝ : StrictOrderedSemiring R
a x y : R
n✝ m : ℕ
h : x < y
hx : 0 ≤ x
n : ℕ
x✝ : 0 < n + 1
⊢ x ^ (n + 1) < y ^ (n + 1)
simpa only [pow_succ'] using
  mul_lt_mul_of_le_of_le' (pow_le_pow_of_le_left hx h.le _) h (pow_pos (hx.trans_lt h) _) hx