Lemma zeroincommringfrac (X : intdom) (S : @submonoid (ringmultmonoid X)) (is : ∏ s : S, (pr1 s != 0)) (x : X) (aa : S) (e : setquotpr (eqrelcommringfrac X S) (x ,, aa) = setquotpr _ (0 ,, unel S)) : x = 0. Proof. intros. set (e' := invweq (weqpathsinsetquot _ _ _) e). simpl in e'. generalize e'. apply (@hinhuniv _ (make_hProp _ (setproperty X _ _))). intro t2. simpl. set (aa0 := pr1 t2). set (a0 := pr1 aa0). set (a := pr1 aa). assert (e2 := pr2 t2). simpl in e2. change (x * 1 * a0 = 0 * a * a0) in e2. rewrite (ringmult0x X _) in e2. rewrite (ringmult0x X _) in e2. rewrite (ringrunax2 X _) in e2. apply (intdomax2r X x a0 e2 (is aa0)). Qed.
Require Import UniMath.Algebra.Groups.