feat(analysis): Cauchy sequence and series lemmas (#7858)
from LTE. Mostly relaxing assumptions from metric to
pseudo-metric and proving some obvious lemmas.
eventually_constant_prod and eventually_constant_sum are duplicated by hand because `to_additive` gets confused by the appearance of `1`.
In `norm_le_zero_iff' {G : Type*} [semi_normed_group G] [separated_space G]` and the following two lemmas the type classes assumptions look silly, but those lemmas are indeed useful in some specific situation in LTE.
