Lemma intdomax2l (X : intdom) (x y : X) (is : x * y = 0) (ne : x != 0) : y = 0. Proof. intros. set (int := intdomax X _ _ is). generalize ne. assert (int' : isaprop (x != 0 → y = 0)). { apply impred. intro. apply (setproperty X _ _). } generalize int. simpl. apply (@hinhuniv _ (make_hProp _ int')). intro ene. induction ene as [ e'' | ne' ]. - induction (ne e''). - intro. apply ne'. Defined.
Require Import UniMath.Algebra.Groups.