proposition: Lemma power_minus : forall x y z Hx Hxz, x[!]y[-]z[//]Hx [=] (x[!]y[//]Hx[/] x[!]z[//]Hx[//]Hxz).
proof: Proof. intros. unfold cg_minus in |- *. astepl (x[!]y[//]Hx[*]x[!][--]z[//]Hx). rstepr (x[!]y[//]Hx[*] ([1][/] _[//]Hxz)). algebra. Qed.
imports: CoRN.transc.Exponential