proposition: Lemma Cseq_cv_div_compat : lv <> 0 -> Cseq_cv (Un /Vn) (lu/lv).
proof: Proof. intro Hlu ; unfold Cseq_div, Rdiv. apply Cseq_cv_eq_compat with (Un *(/Vn)). reflexivity. apply Cseq_cv_mult_compat. assumption. apply Cseq_cv_inv_compat ; assumption. Qed.
imports: MyReals PeanoNat Rsequence_def Rsequence_facts Rsequence_base_facts Lia Lra Complex Csequence_def