fact: Definition Cseq_asymptotic P := forall (Q : Cseq -> Prop) Un, (forall Vn, Q Vn -> P Vn) -> Cseq_eventually Q Un -> P Un.
imports: MyReals PeanoNat Rsequence_def Rsequence_facts Rsequence_base_facts Lia Lra Complex Csequence_def