proposition: Lemma nonzeroincommringfrac (X : commring) (S : @submonoid (ringmultmonoid X)) (xa : dirprod X S) (ne : (setquotpr (eqrelcommringfrac X S) xa != setquotpr _ (make_dirprod 0 (unel S)))%type) : (pr1 xa != 0).
proof: Proof. intros. set (x := pr1 xa). set (aa := pr2 xa). assert (e' := negf (weqpathsinsetquot (eqrelcommringfrac X S) _ _) ne). simpl in e'. generalize e'. apply negf. intro e. apply hinhpr. split with (unel S). change (paths (x * 1 * 1) (0 * (pr1 aa) * 1)). rewrite e. repeat rewrite (ringmult0x X _). apply idpath. Defined.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings