proposition: Lemma strong_right_cancel_from_left `{!Commutative op} `{!StrongLeftCancellation op z} : StrongRightCancellation op z.
proof: Proof. intros x y E. rewrite 2!(commutativity _ z). now apply (strong_left_cancellation op z). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra