proposition: Lemma zexp_pos : forall (x : R) x_ z, [0] [<] x -> [0] [<] (x[//]x_) [^^] (z).
proof: Proof. intros. pattern z in |- *. apply Cnats_Z_ind. intros. astepr (x[^]n). apply nexp_resp_pos. assumption. intros. astepr ([1][/] x[^]n[//]nexp_resp_ap_zero n x_). apply div_resp_pos. apply nexp_resp_pos. assumption. apply pos_one. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)