Lemma nonzeroincommringfrac (X : commring) (S : @submonoid (ringmultmonoid X)) (xa : X × S) (ne : (setquotpr (eqrelcommringfrac X S) xa != setquotpr _ (0 ,, unel S))) : pr1 xa != 0. 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. exists (unel S). change (x * 1 * 1 = 0 * pr1 aa * 1). rewrite e. repeat rewrite (ringmult0x X _). apply idpath. Qed.
Require Import UniMath.Algebra.Groups.