case h.e'_3
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f < g
gh : g ≈ h
⊢ h - f = g - f + -(g - h)
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f < g
gh : g ≈ h
⊢ Pos (h - f)
convert pos_add_limZero fg (neg_limZero gh) using 1
no goals
case h.e'_3
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f < g
gh : g ≈ h
⊢ h - f = g - f + -(g - h)
simp