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