Lemma commringfraclunit1 (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : islunit (commringfracop1 X S) (commringfracunel1 X S). 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 : add1int (commringfracunel1int X S) xs = xs). { unfold add1int. unfold commringfracop1int. induction xs as [ x s ]. induction s as [ s iss ]. apply pathsdirprod. - simpl. change (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 (1 * s = s). apply (ringlunax2 X s). } apply (maponpaths (setquotpr R) e0). Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.