Definition intdomneq0andmult (X : intdom) (n m : X) (isn : n != 0) (ism : m != 0) : ((n * m) != 0). Proof. intros. intro e. induction (ism (intdomax2l X n m e isn )). Defined.
Require Import UniMath.Algebra.Groups.