Definition ringmultwithminus1_is {X : UU} {opp1 opp2 : binop X} (is : isringops opp1 opp2) : ∏ (x : X), opp2 (minus1_is_l (ringop1axs_is is) (ringop2axs_is is)) x = grinv_is (ringop1axs_is is) x := isminusmultwithminus1_is_l (ringop1axs_is is) (ringop2axs_is is) (ringdistraxs_is is).