fact: Definition make_isringops {X : UU} {opp1 opp2 : binop X} (H1 : isabgrop opp1) (H2 : ismonoidop opp2) (H3 : isdistr opp1 opp2) : isringops opp1 opp2 := make_dirprod (make_dirprod H1 H2) H3.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions