Redundancies between realseq.v and sequences.v #255
Description
There are redundancies between altreals/realseq.v (which predates MathComp-Analysis) and the newer sequences.v. How should we factorize?
Related issue: "The merge of sequences and sums over general sets (see esum.v and realsum.v)" (copy-paste from the wiki)