proposition: Lemma SFL_interv_right : forall fn r cv y, Boule 0 r y -> Un_cv (fun N:nat => SP fn N y) (SFL_interv fn r cv y).
proof: Proof. intros fn r cv y y_bd ; unfold SFL_interv ; case (Rlt_le_dec y r) ; intro y_bd1. case (Rlt_le_dec (- r) y) ; intro y_bd2. destruct (cv y (Rabs_def1 (y - 0) r (eq_ind_r (fun r0 : R => r0 < r) y_bd1 (Rminus_0_r y)) (eq_ind_r (fun r0 : R => - r < r0) y_bd2 (Rminus_0_r y)))) as (l', Hl'). assumption. clear -y_bd y_bd1 y_bd2 ; destruct (Rabs_def2 _ _ y_bd) as [H1 H2] ; rewrite Rminus_0_r in H1, H2 ; apply False_ind ; apply Rlt_irrefl with (-r) ; apply Rlt_le_trans with y ; assumption. clear -y_bd y_bd1; destruct (Rabs_def2 _ _ y_bd) as [H1 H2] ; rewrite Rminus_0_r in H1, H2 ; apply False_ind ; apply Rlt_irrefl with y ; apply Rlt_le_trans with r ; assumption. Qed.
imports: Reals RFsequence Lra PeanoNat