proposition: Lemma islcancelableif {X : hSet} (opp : binop X) (x : X) (is : ∏ a b : X, paths (opp x a) (opp x b) -> a = b) : islcancelable opp x.
proof: Proof. intros. apply isinclbetweensets. - apply (setproperty X). - apply (setproperty X). - apply is. Defined.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings