proposition: Lemma exp_form : forall (x y:R) (n:nat), (0 < n)%nat -> E1 x n * E1 y n - Reste_E x y n = E1 (x + y) n.
proof: Proof. intros; unfold E1. rewrite cauchy_finite. - unfold Reste_E; unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_r; apply sum_eq; intros. rewrite binomial. rewrite scal_sum; apply sum_eq; intros. unfold C; unfold Rdiv; repeat rewrite Rmult_assoc; rewrite (Rmult_comm (INR (fact i))); repeat rewrite Rmult_assoc; rewrite Rinv_l. + rewrite Rmult_1_r; rewrite Rinv_mult. ring. + apply INR_fact_neq_0. - apply H. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lia Lra