Lemma mult0x_is_l {X : UU} {opp1 opp2 : binop X} (is1 : isgrop opp1) (is2 : ismonoidop opp2) (is12 : isdistr opp1 opp2) (x : X) : opp2 (unel_is (pr1 is1)) x = unel_is (pr1 is1). Proof. induction is12 as [ ldistr0 rdistr0 ]. induction is2 as [ assoc2 [ un2 [ lun2 run2 ] ] ]. simpl in *. apply (invmaponpathsweq (make_weq _ (isweqrmultingr_is is1 (opp2 un2 x)))). simpl. induction is1 as [ [ assoc1 [ un1 [ lun1 run1 ] ] ] [ inv0 [ linv0 rinv0 ] ] ]. unfold unel_is. simpl in *. rewrite (lun1 (opp2 un2 x)). induction (rdistr0 un1 un2 x). rewrite (lun2 x). rewrite (lun1 un2). rewrite (lun2 x). apply idpath. Defined.