proposition: Lemma reste1_cv_R0 : forall x y:R, Un_cv (Reste1 x y) 0.
proof: Proof. intros. assert (H := Majxy_cv_R0 x y). unfold Un_cv in H; unfold Rdist in H. unfold Un_cv; unfold Rdist; intros. elim (H eps H0); intros N0 H1. exists (S N0); intros. unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r. apply Rle_lt_trans with (Rabs (Majxy x y (pred n))). - rewrite (Rabs_right (Majxy x y (pred n))). + apply reste1_maj. apply Nat.lt_le_trans with (S N0). * apply Nat.lt_0_succ. * assumption. + apply Rle_ge. unfold Majxy. unfold Rdiv; apply Rmult_le_pos. * apply pow_le. apply Rle_trans with 1. -- left; apply Rlt_0_1. -- apply RmaxLess1. * left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. - replace (Majxy x y (pred n)) with (Majxy x y (pred n) - 0); [ idtac | ring ]. apply H1. unfold ge; apply le_S_n. replace (S (pred n)) with n. + assumption. + symmetry; apply Nat.lt_succ_pred with 0%nat. apply Nat.lt_le_trans with (S N0); [ apply Nat.lt_0_succ | assumption ]. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_def Cos_rel Lia Lra