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