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). apply (strong_left_cancellation op z);trivial. Qed.
imports: HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.interfaces.abstract_algebra