proposition: Lemma abmonoidfrac_setquotpr_equiv {X : abmonoid} {Y : @submonoid X} : ∏ (k : Y) (x : X) (y : Y), setquotpr (binopeqrelabmonoidfrac X Y) (x,,y) = setquotpr (binopeqrelabmonoidfrac X Y) (x * pr1 k,, @op Y y k).
proof: Proof. intros k x y. apply iscompsetquotpr, hinhpr. exists y ; simpl. rewrite !(assocax X) ; apply maponpaths. rewrite commax, !assocax. reflexivity. Qed.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups