mathlib3

e469260a - chore(data/real/cau_seq): generalize to noncommutative settings (#17785)

chore(data/real/cau_seq): generalize to noncommutative settings (#17785) The generalizations are all trivial algebra manipulations, just done in a slightly more careful order to avoid needing commutativity. Many of the results about `cau_seq` were already stated without commutativity assumptions, this just propagates the weakening to downstream results.