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