proposition: Lemma intdomiscancelable (X : intdom) (x : X) (is : x != 0) : iscancelable (@op2 X) x.
proof: Proof. intros. apply iscancelableif. - intros a b. apply (intdomlcan X a b x is). - intros a b. apply (intdomrcan X a b x is). Defined.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings