proposition: Lemma maj_Reste_cv_R0 : forall x y:R, Un_cv (maj_Reste_E x y) 0.
proof: Proof. intros; assert (H := Majxy_cv_R0 x y). unfold Un_cv in H; unfold Un_cv; intros. cut (0 < eps / 4); [ intro | unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. elim (H _ H1); intros N0 H2. exists (max (2 * S N0) 2); intros. unfold Rdist in H2; unfold Rdist; rewrite Rminus_0_r; unfold Majxy in H2; unfold maj_Reste_E. set (M := Rmax 1 (Rmax (Rabs x) (Rabs y))) in *. assert (HM1 : 1 <= M) by apply RmaxLess1. assert (HMx : Rabs x <= M) by (eapply Rle_trans;[apply RmaxLess1|apply RmaxLess2]). assert (HMy : Rabs y <= M) by (eapply Rle_trans;[apply RmaxLess2|apply RmaxLess2]). pose proof (Rabs_pos x) as HPosAbsx. pose proof (Rabs_pos y) as HPosAbsy. rewrite Rabs_right. 2:{ apply Rle_ge. unfold Rdiv; apply Rmult_le_pos. { left; prove_sup0. } apply Rmult_le_pos. { apply pow_le. lra. } left; apply Rinv_0_lt_compat; apply Rsqr_pos_lt; apply INR_fact_neq_0. } apply Rle_lt_trans with (4 * (M ^ (4 * S (Nat.div2 (pred n))) / INR (fact (Nat.div2 (pred n))))). - apply Rmult_le_compat_l. { left; prove_sup0. } unfold Rdiv, Rsqr; rewrite Rinv_mult. rewrite (Rmult_comm (M ^ (2 * n))); rewrite (Rmult_comm (M ^ (4 * S (Nat.div2 (pred n))))) ; rewrite Rmult_assoc; apply Rmult_le_compat_l. { left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. } apply Rle_trans with (M ^ (2 * n)). { rewrite Rmult_comm; pattern (M ^ (2 * n)) at 2; rewrite <- Rmult_1_r; apply Rmult_le_compat_l. { apply pow_le; lra. } apply Rmult_le_reg_l with (INR (fact (Nat.div2 (pred n)))). { apply INR_fact_lt_0. } rewrite Rmult_1_r; rewrite Rinv_r. { apply (le_INR 1). apply Nat.le_succ_l. apply INR_lt. apply INR_fact_lt_0. } apply INR_fact_neq_0. } apply Rle_pow. { apply RmaxLess1. } assert (H4 := even_odd_cor n). elim H4; intros N1 H5. elim H5; intro. { assert (0 < N1)%nat by lia. rewrite H6. replace (pred (2 * N1)) with (S (2 * pred N1)) by lia. rewrite div2_S_double. lia. } rewrite H6. replace (pred (S (2 * N1))) with (2 * N1)%nat by lia. rewrite div2_double. lia. - apply Rmult_lt_reg_l with (/ 4). { apply Rinv_0_lt_compat; prove_sup0. } rewrite <- Rmult_assoc; rewrite Rinv_l. 2:discrR. rewrite Rmult_1_l; rewrite Rmult_comm. replace (M ^ (4 * S (Nat.div2 (pred n))) / INR (fact (Nat.div2 (pred n)))) with (Rabs (M ^ (4 * S (Nat.div2 (pred n))) / INR (fact (Nat.div2 (pred n))) - 0)). 2:{ rewrite Rminus_0_r; apply Rabs_right. apply Rle_ge. unfold Rdiv; apply Rmult_le_pos. { apply pow_le. lra. } left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. } apply H2; unfold ge. assert (2 * S N0 <= n)%nat by lia. apply le_S_n. apply INR_le; apply Rmult_le_reg_l with (INR 2). { simpl; prove_sup0. } do 2 rewrite <- mult_INR; apply le_INR. apply Nat.le_trans with n. { apply H4. } assert (H5 := even_odd_cor n). elim H5; intros N1 H6. elim H6; intro. { assert (0 < N1)%nat by lia. rewrite H7. apply Nat.mul_le_mono_nonneg_l. { apply Nat.le_0_l. } replace (pred (2 * N1)) with (S (2 * pred N1)) by lia. rewrite div2_S_double. lia. } rewrite H7. change (pred (S (2 * N1))) with (2 * N1)%nat. rewrite div2_double. lia. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lia Lra