proposition: Lemma Majxy_cv_R0 : forall x y:R, Un_cv (Majxy x y) 0.
proof: Proof. intros. set (C := Rmax 1 (Rmax (Rabs x) (Rabs y))). set (C0 := C ^ 4). assert (0 < C). { apply Rlt_le_trans with 1. - apply Rlt_0_1. - unfold C. apply RmaxLess1. } assert (0 < C0) by (unfold C0; apply pow_lt; assumption). assert (H1 := cv_speed_pow_fact C0). unfold Un_cv in H1; unfold Rdist in H1. unfold Un_cv; unfold Rdist; intros. cut (0 < eps / C0); [ intro | unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; assumption ] ]. elim (H1 (eps / C0) H3); intros N0 H4. exists N0; intros. replace (Majxy x y n) with (C0 ^ S n / INR (fact n)). 2:{ unfold Majxy. unfold C0. rewrite pow_mult. unfold C; reflexivity. } simpl. apply Rmult_lt_reg_l with (Rabs (/ C0)). { apply Rabs_pos_lt. apply Rinv_neq_0_compat. lra. } rewrite <- Rabs_mult. unfold Rminus; rewrite Rmult_plus_distr_l. rewrite Ropp_0; rewrite Rmult_0_r. unfold Rdiv; repeat rewrite <- Rmult_assoc. rewrite Rinv_l. 2:nra. rewrite Rmult_1_l. rewrite (Rabs_right (/ C0)). 2:apply Rle_ge; left; apply Rinv_0_lt_compat; assumption. rewrite <- (Rmult_comm eps). replace (C0 ^ n * / INR (fact n) + 0) with (C0 ^ n * / INR (fact n) - 0) by ring. unfold Rdiv in H4; apply H4; assumption. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_def Cos_rel Lia Lra