proposition: Lemma isgrdirprod (X Y : gr) : isgrop (@op (setwithbinopdirprod X Y)).
proof: Proof. split with (ismonoiddirprod X Y). split with (λ xy : _, make_dirprod (grinv X (pr1 xy)) (grinv Y (pr2 xy))). split. - intro xy. destruct xy as [ x y ]. unfold unel_is. simpl. apply pathsdirprod. apply (grlinvax X x). apply (grlinvax Y y). - intro xy. destruct xy as [ x y ]. unfold unel_is. simpl. apply pathsdirprod. apply (grrinvax X x). apply (grrinvax Y y). Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids