proposition: Lemma isrinvmultwithminus1_is_l {X : UU} {opp1 opp2 : binop X} (is1 : isgrop opp1) (is2 : ismonoidop opp2) (is12 : isdistr opp1 opp2) (x : X) : paths (opp1 x (opp2 (minus1_is_l is1 is2) x)) (unel_is (pr1 is1)).
proof: Proof. set (xinv := opp2 (minus1_is_l is1 is2) x). rewrite (pathsinv0 (lunax_is is2 x)). unfold xinv. rewrite (pathsinv0 (pr2 is12 _ _ x)). unfold minus1_is_l. unfold grinv_is. rewrite (grrinvax_is is1 _). apply mult0x_is_l. apply is2. apply is12. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions