proposition: Lemma Rpower_Rlog : forall x y:R, x <> 1 -> 0 < x -> 0 < y -> Rpower x (Rlog x y) = y.
proof: Proof. intros x y H_neq_x_1 H_lt_0_x H_lt_0_y. unfold Rpower. unfold Rlog. unfold Rdiv. rewrite (Rmult_assoc (ln y) (/ln x) (ln x)). rewrite (Rinv_l (ln x) (ln_neq_0 x H_neq_x_1 H_lt_0_x)). rewrite (Rmult_1_r (ln y)). exact (exp_ln y H_lt_0_y). Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra