Lemma isringopsif {X : UU} {opp1 opp2 : binop X} (is1 : isgrop opp1) (is2 : ismonoidop opp2) (is12 : isdistr opp1 opp2) : isringops opp1 opp2. Proof. set (assoc1 := pr1 (pr1 is1)). split. - split. + exists is1. intros x y. apply (invmaponpathsweq (make_weq _ (isweqrmultingr_is is1 (opp2 (minus1_is_l is1 is2) (opp1 x y))))). simpl. rewrite (isrinvmultwithminus1_is_l is1 is2 is12 (opp1 x y)). rewrite (pr1 is12 x y _). induction (assoc1 (opp1 y x) (opp2 (minus1_is_l is1 is2) x) (opp2 (minus1_is_l is1 is2) y)). rewrite (assoc1 y x _). induction (!isrinvmultwithminus1_is_l is1 is2 is12 x). unfold unel_is. rewrite (runax_is (pr1 is1) y). rewrite (isrinvmultwithminus1_is_l is1 is2 is12 y). apply idpath. + apply is2. - apply is12. Defined.