Lemma intdomiscancelable (X : intdom) (x : X) (is : x != 0) : iscancelable (@op2 X) x. 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.
Require Import UniMath.Algebra.Groups.