no goals
F : Type ?u.10833
ι : Type ?u.10836
α : Type u_1
β : Type ?u.10842
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℕ
⊢ 0 ≤ ↑↑n ↔ 0 ≤ ↑n
simp
F : Type ?u.10833
ι : Type ?u.10836
α : Type u_1
β : Type ?u.10842
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℕ
this : -↑n < 1
⊢ 0 ≤ ↑-[n+1] ↔ 0 ≤ -[n+1]
F : Type ?u.10833
ι : Type ?u.10836
α : Type u_1
β : Type ?u.10842
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℕ
⊢ 0 ≤ ↑-[n+1] ↔ 0 ≤ -[n+1]
have : -(n : α) < 1 := lt_of_le_of_lt (by simp) zero_lt_one
no goals
F : Type ?u.10833
ι : Type ?u.10836
α : Type u_1
β : Type ?u.10842
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℕ
this : -↑n < 1
⊢ 0 ≤ ↑-[n+1] ↔ 0 ≤ -[n+1]
simpa [(negSucc_lt_zero n).not_le, ← sub_eq_add_neg, le_neg] using this.not_le
no goals
F : Type ?u.10833
ι : Type ?u.10836
α : Type u_1
β : Type ?u.10842
inst✝¹ : OrderedRing α
inst✝ : Nontrivial α
n : ℕ
⊢ -↑n ≤ 0
simp