proposition: Lemma R_mult_lft_ext : forall x y z, R_mult x z [#] R_mult y z -> x [#] y.
proof: Proof. intros x y z Hxy. apply zero_minus_apart. apply R_mult_ap_zero' with z. apply ap_wdl_unfolded with (R_mult x z[-]R_mult y z). apply minus_ap_zero; auto. apply eq_symmetric_unfolded. eapply eq_transitive_unfolded. apply R_mult_comm. eapply eq_transitive_unfolded. apply R_mult_dist_minus. apply cg_minus_wd; apply R_mult_comm. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection