proposition: Lemma isassocdirprod (X Y : monoid) : isassoc (@op (setwithbinopdirprod X Y)).
proof: Proof. simpl. intros xy xy' xy''. simpl. apply pathsdirprod. - apply (assocax X). - apply (assocax Y). Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders