Lemma intdomrcan (X : intdom) : ∏ (a b c : X), c != 0 → a * c = b * c → a = b. Proof. intros a b c ne e. apply (@grtopathsxy X a b). change (a - b = 0). assert (e' := grfrompathsxy X e). change (a * c - b * c = 0) in e'. rewrite <- (ringlmultminus X _ _) in e'. rewrite <- (ringrdistr X _ _ c) in e'. set (int := intdomax X _ _ e'). generalize ne. assert (int' : isaprop (c != 0 → a - b = 0)). { apply impred. intro. apply (setproperty X _ _). } generalize int. simpl. apply (@hinhuniv _ (make_hProp _ int')). intro ene. induction ene as [ e'' | ne' ]. - intro. apply e''. - induction (ne ne'). Qed.
Require Import UniMath.Algebra.Groups.