proposition: Lemma nexp_distr_recip : forall (x : R) n x_ xn_, ([1][/] x[//]x_) [^]n [=] ([1][/] x[^]n[//]xn_).
proof: Proof. intros. induction n as [| n Hrecn]; intros. simpl in |- *. algebra. astepl (([1][/] x[//]x_)[^]n[*] ([1][/] x[//]x_)). cut (x[^]n [#] [0]). intro H. astepl (([1][/] x[^]n[//]H)[*] ([1][/] x[//]x_)). cut (x[^]n[*]x [#] [0]). intro H2. rstepl ([1][/] x[^]n[*]x[//]H2). apply div_wd; algebra. apply mult_resp_ap_zero; auto. apply nexp_resp_ap_zero. auto. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)