proposition: Lemma ln_pow : forall (x : R), 0 < x -> forall (n : nat), ln (x^n) = (INR n)*(ln x).
proof: Proof. intros x Hx. induction n as [|m Hm]. + simpl. rewrite ln_1. exact (eq_sym (Rmult_0_l (ln x))). + unfold pow. fold pow. rewrite (ln_mult x (x^m) Hx (pow_lt x m Hx)). rewrite Hm. rewrite <- (Rmult_1_l (ln x)) at 1. rewrite <- (Rmult_plus_distr_r 1 (INR m) (ln x)). rewrite (Rplus_comm 1 (INR m)). destruct m as [|m]; simpl. - lra. - reflexivity. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra