proposition: Lemma zeroincommringfrac (X : intdom) (S : @submonoid (ringmultmonoid X)) (is : ∏ s : S, (pr1 s != 0)) (x : X) (aa : S) (e : paths (setquotpr (eqrelcommringfrac X S) (make_dirprod x aa)) (setquotpr _ (make_dirprod 0 (unel S)))) : x = 0.
proof: 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 (paths (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)). Defined.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings