proposition: Lemma zexp_inv_nexp' : forall (x : R) (n : nat) x_ xn_, (x[//]x_) [^^] (- n) [=] ([1][/] x[^]n[//]xn_).
proof: Proof. intros x n Hx H1. astepl (([1][/] x[//]Hx) [^]n). astepr ([1][^]n[/] x[^]n[//]H1). apply nexp_distr_div. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)