proposition: Lemma zexp_inv : forall (x : R) x_ m xm_, (x[//]x_) [^^] (- m) [=] ([1][/] (x[//]x_) [^^] (m) [//]xm_).
proof: Proof. intros x Hx m. pattern m in |- *. apply nats_Z_ind. intros. apply eq_transitive_unfolded with ([1][/] x[^]n[//]nexp_resp_ap_zero n Hx). apply zexp_inv_nexp'. apply div_wd. algebra. algebra. intros. rewrite Z.opp_involutive. astepl (x[^]n). astepl ((x[^]n) [/]OneNZ). apply eq_div. astepl (x[^]n[*] ([1][/] x[//]Hx) [^]n). astepl ((x[*] ([1][/] x[//]Hx)) [^]n). astepr ([1]:R). astepr (([1]:R) [^]n). apply nexp_wd. algebra. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)