x y : ℝ
a b : Cauchy abs
⊢ { cauchy := a } + -{ cauchy := b } = { cauchy := a } - { cauchy := b }
x y : ℝ
a b : Cauchy abs
⊢ { cauchy := a - b } = { cauchy := a } - { cauchy := b }
rw [sub_eq_add_neg, ofCauchy_add, ofCauchy_neg]
no goals
x y : ℝ
a b : Cauchy abs
⊢ { cauchy := a } + -{ cauchy := b } = { cauchy := a } - { cauchy := b }
rfl