case h.e'_3
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f < g
gh : g < h
⊢ h - f = g - f + (h - g)
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f < g
gh : g < h
⊢ Pos (h - f)
convert add_pos fg 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 + (h - g)
simp