proposition: Lemma multx0_is_l {X : UU} {opp1 opp2 : binop X} (is1 : isgrop opp1) (is2 : ismonoidop opp2) (is12 : isdistr opp1 opp2) (x : X) : paths (opp2 x (unel_is (pr1 is1))) (unel_is (pr1 is1)).
proof: Proof. destruct is12 as [ ldistr0 rdistr0 ]. destruct is2 as [ assoc2 [ un2 [ lun2 run2 ] ] ]. simpl in *. apply (invmaponpathsweq (make_weq _ (isweqrmultingr_is is1 (opp2 x un2)))). simpl. destruct is1 as [ [ assoc1 [ un1 [ lun1 run1 ] ] ] [ inv0 [ linv0 rinv0 ] ] ]. unfold unel_is. simpl in *. rewrite (lun1 (opp2 x un2)). destruct (ldistr0 un1 un2 x). rewrite (run2 x). rewrite (lun1 un2). rewrite (run2 x). apply idpath. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions