proposition: Lemma SFL_interv_right : forall fn r cv y, Boule 0 r y -> Cseq_cv (fun N:nat => CFpartial_sum (fun n => fn n y) N) (SFL_interv fn r cv y).
proof: Proof. intros fn r cv z z_bd ; unfold SFL_interv ; destruct (Rlt_le_dec (Cnorm (0 - z)) r) as [z_bd2 | z_lb]. destruct (cv z z_bd2) as [l Hl] ; assumption. assert (Hf : Cnorm (0 - z) < Cnorm (0 - z)). apply Rlt_le_trans with r ; unfold Boule in * ; assumption. elim (Rlt_irrefl _ Hf). Qed.
imports: Rsequence_def Rinterval Ranalysis_def Rsequence_cv_facts Rsequence_tactics MyRIneq Cfunctions Csequence Csequence_facts CFsequence Cnorm Cprop_base Ctacfield Lia Lra PeanoNat Cmet Canalysis_def Canalysis_deriv