proposition: Lemma ln_pow x n : 0 < x -> ln (x^n) = INR n * ln x.
proof: Proof. intro Hx ; induction n as [ | n IH]. rewrite pow_O ln_1 ; simpl ; ring. rewrite S_INR ; simpl ; rewrite ln_mult ; try intuition. rewrite IH ; ring. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)