proposition: Lemma Rlog_pow : forall (x : R) (n : nat), x <> 1 -> 0 < x -> Rlog x (x^n) = INR n.
proof: Proof. intros x n H_neq_x_1 H_lt_0_x. rewrite <- (Rpower_pow n x H_lt_0_x). unfold Rpower. unfold Rlog. rewrite (ln_exp (INR n * ln x)). unfold Rdiv. rewrite (Rmult_assoc (INR n) (ln x) (/ln x)). rewrite (Rinv_r (ln x) (ln_neq_0 x H_neq_x_1 H_lt_0_x)). exact (Rmult_1_r (INR n)). Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra