fact: Definition ispartrdistr {X : abmonoid} (Y : @submonoid X) (opp1 opp2 : binop X) := ∏ (x y : X) (k : Y), opp2 (opp1 x y) (pr1 k) = opp1 (opp2 x (pr1 k)) (opp2 y (pr1 k)).
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups