proposition: Lemma Rseq_cv_continuity_interval_compat : forall Un lu f a b, interval a b lu -> (forall n, interval a b (Un n)) -> Rseq_cv Un lu -> continuity_interval a b f -> Rseq_cv (fun n => f (Un n)) (f lu).
proof: Proof. intros Un lu f a b lu_in Un_in Hu Hf eps eps_pos. destruct (Hf _ lu_in _ eps_pos) as [h [h_pos Hh]] ; simpl in Hh. destruct (Hu _ h_pos) as [N HN] ; exists N ; intros n n_lb. destruct (Req_dec lu (Un n)) as [Heq | Hneq]. rewrite Heq, R_dist_eq ; assumption. apply Hh ; split ; [apply Un_in | apply HN ; assumption]. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra