α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
K : α
H : ∀ (i : ℕ), abs (↑f i) < K
i : ℕ
x✝ : i ≥ 0
⊢ ↑f i ≤ K
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
K : α
H : ∀ (i : ℕ), abs (↑f i) < K
i : ℕ
x✝ : i ≥ 0
⊢ 1 ≤ ↑(const (K + 1) - f) i
rw [sub_apply, const_apply, le_sub_iff_add_le', add_le_add_iff_right]
no goals
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
K : α
H : ∀ (i : ℕ), abs (↑f i) < K
i : ℕ
x✝ : i ≥ 0
⊢ ↑f i ≤ K
exact le_of_lt (abs_lt.1 (H _)).2