α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f ≈ g
gh : g < h
this : Pos (h - g + -(f - g))
⊢ f < h
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f ≈ g
gh : g < h
⊢ f < h
have := pos_add_limZero gh (neg_limZero fg)
no goals
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f ≈ g
gh : g < h
this : Pos (h - g + -(f - g))
⊢ f < h
rwa [← sub_eq_add_neg, sub_sub_sub_cancel_right] at this