proposition: Lemma power_mult : forall x y z Hx Hxy, x[!]y[*]z[//]Hx [=] (x[!]y[//]Hx) [!]z[//]Hxy.
proof: Proof. intros; unfold power in |- *. apply Exp_wd. astepl (z[*]y[*]Log x Hx). astepl (z[*] (y[*]Log x Hx)). algebra. Qed.
imports: CoRN.transc.Exponential