`{!Commutative op} `{!StrongLeftCancellation op z} : StrongRightCancellation op z. Proof. intros x y E. rewrite 2!(commutativity _ z). apply (strong_left_cancellation op z);trivial. Qed.
Require Import Require Import