proposition: Lemma commringfraclunit1 (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : islunit (commringfracop1 X S) (commringfracunel1 X S).
proof: Proof. intros. set (R := eqrelcommringfrac X S). set (add1int := commringfracop1int X S). set (add1 := commringfracop1 X S). set (un1 := commringfracunel1 X S). unfold islunit. apply (setquotunivprop R (λ x, _ = _)). intro xs. assert (e0 : paths (add1int (commringfracunel1int X S) xs) xs). { unfold add1int. unfold commringfracop1int. destruct xs as [ x s ]. destruct s as [ s iss ]. apply pathsdirprod. - simpl. change (paths ((s * 0) + (1 * x)) x). rewrite (@ringmultx0 X s). rewrite (ringlunax2 X x). rewrite (ringlunax1 X x). apply idpath. - apply (invmaponpathsincl _ (isinclpr1carrier (pr1 S))). change (paths (1 * s) s). apply (ringlunax2 X s). } apply (maponpaths (setquotpr R) e0). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids