proposition: Lemma ln_Rpower x y (Hx : 0 < x) (Hy : 0 <= y) : ln (Rpower x y) = y * ln x.
proof: Proof. rewrite /Rpower // . by rewrite ln_exp. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval