proposition: Lemma right_cancel_from_left `{!Setoid A} `{!Commutative op} `{!LeftCancellation op z} : RightCancellation op z.
proof: Proof. intros x y E. apply (left_cancellation op z). now rewrite 2!(commutativity z _). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra