proposition: Lemma zexp_resp_ap_zero : forall (x : R) m x_, (x[//]x_) [^^] (m) [#] [0].
proof: Proof. intros. pattern m in |- *. apply Cnats_Z_ind. intros. astepl (x[^]n). apply nexp_resp_ap_zero. assumption. intro. astepl (([1][/] x[//]x_) [^]n). apply nexp_resp_ap_zero. apply div_resp_ap_zero_rev. algebra. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)