proposition: Lemma zexp_strext : forall (x y : R) m x_ y_, (x[//]x_) [^^] (m) [#] (y[//]y_) [^^] (m) -> x [#] y.
proof: Proof. intros x y m Hx Hy. pattern m in |- *. apply Cnats_Z_ind. intros. apply (nexp_strong_ext R n). change (x[^]n [#] y[^]n) in |- *. astepl (x[//]Hx)[^^] (n). astepr (y[//]Hy)[^^] (n). auto. intros. apply (nexp_strong_ext R n). change (x[^]n [#] y[^]n) in |- *. cut (([1][/] x[^]n[//]nexp_resp_ap_zero n Hx) [#] ([1][/] y[^]n[//]nexp_resp_ap_zero n Hy)). intro H0. generalize (div_strext _ _ _ _ _ _ _ H0); intro. elim X0; intros H2. elim (ap_irreflexive_unfolded _ _ H2). assumption. astepl (x[//]Hx)[^^] (- n). astepr (y[//]Hy)[^^] (- n). auto. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)