proposition: Lemma reste_cv_R0 : forall x y:R, Un_cv (Reste x y) 0.
proof: Proof. intros. unfold Reste. set (An := fun n:nat => Reste2 x y n). set (Bn := fun n:nat => Reste1 x y (S n)). cut (Un_cv (fun n:nat => An n - Bn n) (0 - 0) -> Un_cv (fun N:nat => Reste2 x y N - Reste1 x y (S N)) 0). - intro. apply H. apply CV_minus. + unfold An. replace (fun n:nat => Reste2 x y n) with (Reste2 x y). * apply reste2_cv_R0. * reflexivity. + unfold Bn. assert (H0 := reste1_cv_R0 x y). unfold Un_cv in H0; unfold Rdist in H0. unfold Un_cv; unfold Rdist; intros. elim (H0 eps H1); intros N0 H2. exists N0; intros. apply H2. unfold ge; apply Nat.le_trans with (S N0). * apply Nat.le_succ_diag_r. * apply -> Nat.succ_le_mono; assumption. - unfold An, Bn. intro. replace 0 with (0 - 0); [ idtac | ring ]. exact H. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_def Cos_rel Lia Lra