Definition make_isrigops {X : UU} {opp1 opp2 : binop X} (H1 : isabmonoidop opp1) (H2 : ismonoidop opp2) (H3 : ∏ x : X, (opp2 (unel_is H1) x) = (unel_is H1)) (H4 : ∏ x : X, (opp2 x (unel_is H1)) = (unel_is H1)) (H5 : isdistr opp1 opp2) : isrigops opp1 opp2 := ((H1 ,, H2) ,, H3 ,, H4) ,, H5.