Definition intdomnonzerosubmonoid (X : intdom) : @subabmonoid (ringmultabmonoid X). Proof. intros. exists (λ x : X, make_hProp _ (isapropneg (x = 0))). split. - intros a b. simpl in *. intro e. set (int := intdomax X (pr1 a) (pr1 b) e). clearbody int. generalize int. apply toneghdisj. apply (pr2 a ,, pr2 b). - simpl. apply (nonzeroax X). Defined.
Require Import UniMath.Algebra.Groups.