proposition: Lemma intdomax2r (X : intdom) (x y : X) (is : paths (x * y) 0) (ne : y != 0) : x = 0.
proof: Proof. intros. set (int := intdomax X _ _ is). generalize ne. assert (int' : isaprop (y != 0 -> x = 0)). { apply impred. intro. apply (setproperty X _ _). } generalize int. simpl. apply (@hinhuniv _ (make_hProp _ int')). intro ene. destruct ene as [ e'' | ne' ]. - intro. apply e''. - destruct (ne ne'). Defined.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings