proposition: Lemma power_recip : forall x q Hx (Hx' : [0] [<=] x) Hq (Hq' : 0 < q), x[!][1][/] nring q[//]Hq[//]Hx [=] NRoot Hx' Hq'.
proof: Proof. intros. apply NRoot_unique. apply less_leEq; apply power_pos. apply power_pos. astepr (x[!][1][//]Hx). astepl (_[!]nring q[//]power_pos _ ([1][/] _[//]Hq) Hx). Step_final (x[!] ([1][/] _[//]Hq) [*]nring q[//]Hx). Qed.
imports: CoRN.transc.Exponential