fact: Definition iscommringopstoiscommrigops (X : UU) (opp1 opp2 : binop X) (is : iscommringops opp1 opp2) : iscommrigops opp1 opp2 := make_dirprod (isringopstoisrigops _ _ _ (pr1 is)) (pr2 is).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions