Definition isringopstoisrigops (X : UU) (opp1 opp2 : binop X) (is : isringops opp1 opp2) : isrigops opp1 opp2. Proof. split. - exists (isabgroptoisabmonoidop _ _ (ringop1axs_is is) ,, ringop2axs_is is). split. + simpl. apply (ringmult0x_is). + simpl. apply (ringmultx0_is). - apply (ringdistraxs_is is). Defined.