x y : ℝ
a b : Cauchy abs
⊢ ({ cauchy := a } - { cauchy := b }).cauchy = ({ cauchy := a } + -{ cauchy := b }).cauchy
x y : ℝ
a b : Cauchy abs
⊢ ({ cauchy := a } - { cauchy := b }).cauchy = { cauchy := a }.cauchy - { cauchy := b }.cauchy
rw [sub_eq_add_neg, ← cauchy_neg, ← cauchy_add]
no goals
x y : ℝ
a b : Cauchy abs
⊢ ({ cauchy := a } - { cauchy := b }).cauchy = ({ cauchy := a } + -{ cauchy := b }).cauchy
rfl