Lemma isminusmultwithminus1_is_l {X : UU} {opp1 opp2 : binop X} (is1 : isgrop opp1) (is2 : ismonoidop opp2) (is12 : isdistr opp1 opp2) (x : X) : opp2 (minus1_is_l is1 is2) x = grinv_is is1 x. Proof. apply (invmaponpathsweq (make_weq _ (isweqrmultingr_is is1 x))). simpl. rewrite (islinvmultwithminus1_is_l is1 is2 is12 x). unfold grinv_is. rewrite (grlinvax_is is1 x). apply idpath. Defined.