proposition: Lemma Rseq_cv_0_abs_compat : forall Un, Rseq_cv (| Un |) 0 -> Rseq_cv Un 0.
proof: Proof. intros Un HUn eps eps_pos ; destruct (HUn _ eps_pos) as [N HN] ; exists N ; intros n n_lb ; apply Rle_lt_trans with (R_dist (|Un| n)%R 0). right ; unfold R_dist, Rseq_abs ; do 2 rewrite Rminus_0_r ; rewrite Rabs_Rabsolu ; reflexivity. apply HN ; assumption. Qed.
imports: Rbase Rsequence Ranalysis Rfunctions Rseries_def Lra RiemannInt SeqProp MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity