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