proposition: Lemma zexp_wd : forall (x y : R) m x_ y_, x [=] y -> (x[//]x_) [^^] (m) [=] (y[//]y_) [^^] (m).
proof: Proof. intros x y m Hx Hy; intros. apply not_ap_imp_eq. intro H0. generalize (zexp_strext _ _ _ _ _ H0); intro. apply (eq_imp_not_ap _ _ _ H). assumption. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)