proposition: Lemma power_int : forall x z Hx Hx', x[!]zring z[//]Hx [=] (x[//]Hx') [^^] (z).
proof: Proof. intros; induction z as [| p| p]. simpl in |- *. Step_final (x[!][0][//]Hx). simpl in |- *. Step_final (x[!]nring (nat_of_P p) [//]Hx). simpl in |- *. astepl (x[!][--] (nring (nat_of_P p)) [//]Hx). astepl ([1][/] x[!]nring (nat_of_P p) [//]Hx[//]Exp_ap_zero _). Step_final ([1][/] x[^]nat_of_P p[//]nexp_resp_ap_zero _ Hx'). Qed.
imports: CoRN.transc.Exponential