proposition: Lemma mult_power : forall x y z Hx Hy Hxy, (x[*]y) [!]z[//]Hxy [=] x[!]z[//]Hx[*]y[!]z[//]Hy.
proof: Proof. intros; unfold power in |- *. astepr (Exp (z[*]Log _ Hx[+]z[*]Log _ Hy)). Step_final (Exp (z[*] (Log _ Hx[+]Log _ Hy))). Qed.
imports: CoRN.transc.Exponential