proposition: Lemma intdomrcan (X : intdom) : ∏ (a b c : X), c != 0 -> paths (a * c) (b * c) -> a = b.
proof: Proof. intros a b c ne e. apply (@grtopathsxy X a b). change (paths (a - b) 0). assert (e' := grfrompathsxy X e). change (paths ((a * c) - (b * c)) 0) in e'. rewrite (pathsinv0 (ringlmultminus X _ _)) in e'. rewrite (pathsinv0 (ringrdistr X _ _ c)) in e'. set (int := intdomax X _ _ e'). generalize ne. assert (int' : isaprop (c != 0 -> paths (a - b) 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