proposition: Lemma pow_exp_ln : forall x n, 0 < x -> x ^ n = exp (n * ln x).
proof: Proof. intros x n H. induction n. simpl. rewrite Rmult_0_l. rewrite exp_0. reflexivity. rewrite S_INR. rewrite Rmult_plus_distr_r. rewrite <- tech_pow_Rmult. rewrite exp_plus. rewrite Rmult_1_l. rewrite exp_ln ; [ | apply H]. rewrite IHn. ring. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics