proposition: Lemma Rseq_cv_continuity_compat : forall Un lu f, Rseq_cv Un lu -> continuity_pt f lu -> Rseq_cv (fun n => f (Un n)) (f lu).
proof: Proof. intros Un lu f Hu Hf eps Heps. destruct (Hf eps) as [h [Hh H]]; [assumption|simpl in H]. destruct (Hu h) as [N HN]; [assumption|]. exists N; intros n Hn. destruct (Req_dec lu (Un n)) as [Heq|Heq]. rewrite Heq; rewrite R_dist_eq; assumption. apply H; split; [compute; tauto|]. apply HN; assumption. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra