mathlib3

60f72157 - chore(data/real/cau_seq_completion): golf using existing lemmas (#16469)

chore(data/real/cau_seq_completion): golf using existing lemmas (#16469) This extracts `cau_seq.mul_equiv_mul` and `cau_seq.sub_equiv_sub` into standalone lemmas, and uses the existing lemmas for `add` and `neg` rather than reproving the result from scratch.