proposition: Lemma R_mult_rht_ext : forall x y z, R_mult x y [#] R_mult x z -> y [#] z.
proof: Proof. intros x y z Hxy. apply R_mult_lft_ext with x. eapply ap_wdl_unfolded. eapply ap_wdr_unfolded. apply Hxy. apply R_mult_comm. apply R_mult_comm. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection