proposition: Lemma abmonoidsbinop_lunax {X Y : abmonoid} (f : monoidfun X Y) : abmonoidshombinop (unelmonoidfun X Y) f = f.
proof: Proof. use monoidfun_paths. use funextfun. intros x. use (lunax Y). Qed.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders