proposition: Lemma nexp_resp_ap_zero : forall (x : R) n, x [#] [0] -> x[^]n [#] [0].
proof: Proof. intros. elim n. simpl in |- *. algebra. intros. simpl in |- *. apply mult_resp_ap_zero. assumption. assumption. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)