β : Type ?u.237030
A : Type ?u.237033
G : Type ?u.237036
M : Type ?u.237039
R : Type u_1
inst✝ : LinearOrderedSemiring R
a✝ b a : R
ha : 0 ≤ a
n : ℕ
hn : n ≠ 0
⊢ a ^ n ≤ 1 → a ≤ 1
β : Type ?u.237030
A : Type ?u.237033
G : Type ?u.237036
M : Type ?u.237039
R : Type u_1
inst✝ : LinearOrderedSemiring R
a✝ b a : R
ha : 0 ≤ a
n : ℕ
hn : n ≠ 0
⊢ a ^ n ≤ 1 ↔ a ≤ 1
refine' ⟨_, pow_le_one n ha⟩
β : Type ?u.237030
A : Type ?u.237033
G : Type ?u.237036
M : Type ?u.237039
R : Type u_1
inst✝ : LinearOrderedSemiring R
a✝ b a : R
ha : 0 ≤ a
n : ℕ
hn : n ≠ 0
⊢ ¬1 < a ^ n → ¬1 < a
β : Type ?u.237030
A : Type ?u.237033
G : Type ?u.237036
M : Type ?u.237039
R : Type u_1
inst✝ : LinearOrderedSemiring R
a✝ b a : R
ha : 0 ≤ a
n : ℕ
hn : n ≠ 0
⊢ a ^ n ≤ 1 → a ≤ 1
rw [← not_lt, ← not_lt]
no goals
β : Type ?u.237030
A : Type ?u.237033
G : Type ?u.237036
M : Type ?u.237039
R : Type u_1
inst✝ : LinearOrderedSemiring R
a✝ b a : R
ha : 0 ≤ a
n : ℕ
hn : n ≠ 0
⊢ ¬1 < a ^ n → ¬1 < a
exact mt fun h => one_lt_pow h hn