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. intros k x y. apply iscompsetquotpr, hinhpr. exists y ; simpl. rewrite !(assocax X) ; apply maponpaths. rewrite commax, !assocax. reflexivity. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.