proposition: Lemma nexp_distr_div : forall (x y : R) n y_ yn_, (x[/] y[//]y_) [^]n [=] (x[^]n[/] y[^]n[//]yn_).
proof: Proof. simple induction n. intros. simpl in |- *. algebra. intros. simpl in |- *. generalize (H y_ (nexp_resp_ap_zero y n0 y_)); intro. astepl ((x[^]n0[/] y[^]n0[//]nexp_resp_ap_zero y n0 y_) [*] (x[/] y[//]y_)). simpl in |- *. rational. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)