proposition: Lemma exp_pow x n : (exp x) ^ n = exp (x* (INR n)).
proof: Proof. induction n. ring_simplify. rewrite Rmult_0_r, exp_0; reflexivity. simpl pow. replace (S n)%R with (n+1)%nat by lia. rewrite plus_INR. replace (INR 1) with R1 by trivial. ring_simplify (x * (INR n + R1)). rewrite exp_plus, IHn. auto with *. Qed.
imports: Reals Rsequence_facts Rseries_def Rseries_facts Rseries_usual Rpser Rintegral RTaylor Lia Lra Wallis