Lemma isrinvmultwithminus1_is_l {X : UU} {opp1 opp2 : binop X} (is1 : isgrop opp1) (is2 : ismonoidop opp2) (is12 : isdistr opp1 opp2) (x : X) : opp1 x (opp2 (minus1_is_l is1 is2) x) = unel_is (pr1 is1). Proof. set (xinv := opp2 (minus1_is_l is1 is2) x). rewrite <- (lunax_is is2 x). unfold xinv. rewrite <- (pr2 is12 _ _ x). unfold minus1_is_l. unfold grinv_is. rewrite (grrinvax_is is1 _). apply mult0x_is_l. apply is2. apply is12. Defined.