proposition: Lemma nexp_distr_div' : forall (x y : R) n y_, (x[/] y[//]y_) [^]n [=] (x[^]n[/] y[^]n[//]nexp_resp_ap_zero y n y_).
proof: Proof. intros. apply nexp_distr_div. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)