proposition: Lemma R_recip_strext : forall x y x_ y_, R_recip x x_ [#] R_recip y y_ -> x [#] y.
proof: Proof. intros. apply zero_minus_apart. apply ap_wdl with (x[*]y[*] (R_recip y y_[-]R_recip x x_)). apply R_integral_domain. apply R_integral_domain; auto. apply minus_ap_zero; apply ap_symmetric_unfolded; auto. stepl (y[*]R_recip y y_[*]x[-]x[*]R_recip x x_[*]y). 2: unfold cg_minus; ring. stepr ([1][*]x[-][1][*]y). 2: unfold cg_minus; ring. apply cg_minus_wd; apply mult_wdl; apply R_recip_inverse. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection