Lemma isrcancelableif {X : hSet} (opp : binop X) (x : X) (is : ∏ a b : X, opp a x = opp b x → a = b) : isrcancelable opp x. Proof. intros. apply isinclbetweensets. - apply (setproperty X). - apply (setproperty X). - apply is. Defined.
Require Import UniMath.Algebra.Groups.