F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
⊢ 0 ≤ ↑n * x + ↑n * ↑n
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
⊢ 0 ≤ ↑n * x + ↑n * ↑n
have hnx : 0 < n → 0 ≤ x + n := fun hn => by
  have := _root_.add_le_add (neg_le_of_abs_le hx) (cast_one_le_of_pos hn)
  rwa [add_left_neg] at this
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
⊢ 0 ≤ ↑n * x + ↑n * ↑n
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
⊢ 0 ≤ ↑n * x + ↑n * ↑n
have hnx' : n < 0 → x + n ≤ 0 := fun hn => by
  have := _root_.add_le_add (le_of_abs_le hx) (cast_le_neg_one_of_neg hn)
  rwa [add_right_neg] at this
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
⊢ 0 ≤ ↑n * x + ↑n * ↑n
rw [← mul_add, mul_nonneg_iff]
case inl
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : n < 0
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0

case inr.inl
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b : ℤ
x : α
hx : abs x ≤ 1
hnx : 0 < 0 → 0 ≤ x + ↑0
hnx' : 0 < 0 → x + ↑0 ≤ 0
⊢ 0 ≤ ↑0 ∧ 0 ≤ x + ↑0 ∨ ↑0 ≤ 0 ∧ x + ↑0 ≤ 0

case inr.inr
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : 0 < n
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
rcases lt_trichotomy n 0 with (h | rfl | h)
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
hn : 0 < n
this : -1 + 1 ≤ x + ↑n
⊢ 0 ≤ x + ↑n
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
hn : 0 < n
⊢ 0 ≤ x + ↑n
have := _root_.add_le_add (neg_le_of_abs_le hx) (cast_one_le_of_pos hn)
no goals
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
hn : 0 < n
this : -1 + 1 ≤ x + ↑n
⊢ 0 ≤ x + ↑n
rwa [add_left_neg] at this
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hn : n < 0
this : x + ↑n ≤ 1 + -1
⊢ x + ↑n ≤ 0
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hn : n < 0
⊢ x + ↑n ≤ 0
have := _root_.add_le_add (le_of_abs_le hx) (cast_le_neg_one_of_neg hn)
no goals
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hn : n < 0
this : x + ↑n ≤ 1 + -1
⊢ x + ↑n ≤ 0
rwa [add_right_neg] at this
no goals
case inl
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : n < 0
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
exact Or.inr ⟨by exact_mod_cast h.le, hnx' h⟩
no goals
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : n < 0
⊢ ↑n ≤ 0
exact_mod_cast h.le
no goals
case inr.inl
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b : ℤ
x : α
hx : abs x ≤ 1
hnx : 0 < 0 → 0 ≤ x + ↑0
hnx' : 0 < 0 → x + ↑0 ≤ 0
⊢ 0 ≤ ↑0 ∧ 0 ≤ x + ↑0 ∨ ↑0 ≤ 0 ∧ x + ↑0 ≤ 0
simp [le_total 0 x]
no goals
case inr.inr
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : 0 < n
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0
exact Or.inl ⟨by exact_mod_cast h.le, hnx h⟩
no goals
F : Type ?u.28613
ι : Type ?u.28616
α : Type u_1
β : Type ?u.28622
inst✝ : LinearOrderedRing α
a b n : ℤ
x : α
hx : abs x ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : 0 < n
⊢ 0 ≤ ↑n
exact_mod_cast h.le