proposition: Lemma zexp_inv1 : forall (x : R) x_ m, (x[//]x_) [^^] (m - 1) [=] ((x[//]x_) [^^] (m) [/] x[//]x_).
proof: Proof. intros x Hx; intros. replace (m - 1)%Z with (- (- m + 1))%Z. astepl ([1][/] (x[//]Hx) [^^] (- m + 1) [//]zexp_resp_ap_zero x (- m + 1) Hx). apply eq_div. astepr ((x[//]Hx) [^^] (m) [*] ((x[//]Hx) [^^] (- m) [*]x)). astepr ((x[//]Hx) [^^] (m) [*] (([1][/] (x[//]Hx) [^^] (m) [//]zexp_resp_ap_zero x m Hx) [*]x)). rational. rewrite Zopp_plus_distr. rewrite Z.opp_involutive. reflexivity. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)