proposition: Lemma Reste_E_cv : forall x y:R, Un_cv (Reste_E x y) 0.
proof: Proof. intros; assert (H := maj_Reste_cv_R0 x y). unfold Un_cv in H; unfold Un_cv; intros; elim (H _ H0); intros. exists (max x0 1); intros. unfold Rdist; rewrite Rminus_0_r. apply Rle_lt_trans with (maj_Reste_E x y n). - apply Reste_E_maj. apply Nat.lt_le_trans with 1%nat. + apply Nat.lt_0_succ. + apply Nat.le_trans with (max x0 1). * apply Nat.le_max_r. * apply H2. - replace (maj_Reste_E x y n) with (Rdist (maj_Reste_E x y n) 0). + apply H1. unfold ge; apply Nat.le_trans with (max x0 1). * apply Nat.le_max_l. * apply H2. + unfold Rdist; rewrite Rminus_0_r; apply Rabs_right. apply Rle_ge; apply Rle_trans with (Rabs (Reste_E x y n)). * apply Rabs_pos. * apply Reste_E_maj. apply Nat.lt_le_trans with 1%nat. -- apply Nat.lt_0_succ. -- apply Nat.le_trans with (max x0 1). ++ apply Nat.le_max_r. ++ apply H2. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lia Lra