proposition: Lemma power_div : forall x p q Hx (Hx' : [0] [<=] x) Hq (Hq' : 0 < q), x[!]nring p[/] nring q[//]Hq[//]Hx [=] (NRoot Hx' Hq') [^]p.
proof: Proof. intros. apply eq_transitive_unfolded with (x[!] ([1][/] _[//]Hq) [*]nring p[//]Hx). apply power_wd; rational. astepr (NRoot Hx' Hq'[!]nring p[//]NRoot_pos _ Hx' _ Hq' Hx). Step_final ((x[!][1][/] _[//]Hq[//]Hx) [!]nring p[//]power_pos _ _ _). Qed.
imports: CoRN.transc.Exponential