β : Type ?u.237881
A : Type ?u.237884
G : Type ?u.237887
M : Type ?u.237890
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.237881
A : Type ?u.237884
G : Type ?u.237887
M : Type ?u.237890
R : Type u_1
inst✝ : LinearOrderedSemiring R
a✝ b a : R
ha : 0 ≤ a
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ a ^ n ↔ 1 ≤ a
refine' ⟨_, fun h => one_le_pow_of_one_le h n⟩
β : Type ?u.237881
A : Type ?u.237884
G : Type ?u.237887
M : Type ?u.237890
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.237881
A : Type ?u.237884
G : Type ?u.237887
M : Type ?u.237890
R : Type u_1
inst✝ : LinearOrderedSemiring R
a✝ b a : R
ha : 0 ≤ a
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ a ^ n → 1 ≤ a
rw [← not_lt, ← not_lt]
no goals
β : Type ?u.237881
A : Type ?u.237884
G : Type ?u.237887
M : Type ?u.237890
R : Type u_1
inst✝ : LinearOrderedSemiring R
a✝ b a : R
ha : 0 ≤ a
n : ℕ
hn : n ≠ 0
⊢ ¬a ^ n < 1 → ¬a < 1
exact mt fun h => pow_lt_one ha h hn