case intro
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ i, ∀ (j : ℕ), j ≥ i → F ≤ ↑f j
H : LimZero g
i : ℕ
h : ∀ (j : ℕ), j ≥ i → F ≤ ↑f j ∧ abs (↑g j) < F / 2
j : ℕ
ij : j ≥ i
h₁ : F ≤ ↑f j
h₂ : abs (↑g j) < F / 2
⊢ F / 2 ≤ ↑(f + g) j
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ i, ∀ (j : ℕ), j ≥ i → F ≤ ↑f j
H : LimZero g
i : ℕ
h : ∀ (j : ℕ), j ≥ i → F ≤ ↑f j ∧ abs (↑g j) < F / 2
j : ℕ
ij : j ≥ i
⊢ F / 2 ≤ ↑(f + g) j
cases' h j ij with h₁ h₂
case intro
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ i, ∀ (j : ℕ), j ≥ i → F ≤ ↑f j
H : LimZero g
i : ℕ
h : ∀ (j : ℕ), j ≥ i → F ≤ ↑f j ∧ abs (↑g j) < F / 2
j : ℕ
ij : j ≥ i
h₁ : F ≤ ↑f j
h₂ : abs (↑g j) < F / 2
this : F + -(F / 2) ≤ ↑f j + ↑g j
⊢ F / 2 ≤ ↑(f + g) j
case intro
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ i, ∀ (j : ℕ), j ≥ i → F ≤ ↑f j
H : LimZero g
i : ℕ
h : ∀ (j : ℕ), j ≥ i → F ≤ ↑f j ∧ abs (↑g j) < F / 2
j : ℕ
ij : j ≥ i
h₁ : F ≤ ↑f j
h₂ : abs (↑g j) < F / 2
⊢ F / 2 ≤ ↑(f + g) j
have := add_le_add h₁ (le_of_lt (abs_lt.1 h₂).1)
no goals
case intro
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ i, ∀ (j : ℕ), j ≥ i → F ≤ ↑f j
H : LimZero g
i : ℕ
h : ∀ (j : ℕ), j ≥ i → F ≤ ↑f j ∧ abs (↑g j) < F / 2
j : ℕ
ij : j ≥ i
h₁ : F ≤ ↑f j
h₂ : abs (↑g j) < F / 2
this : F + -(F / 2) ≤ ↑f j + ↑g j
⊢ F / 2 ≤ ↑(f + g) j
rwa [← sub_eq_add_neg, sub_self_div_two] at this