fact: Definition rigmultx0_is {X : UU} {opp1 opp2 : binop X} (is : isrigops opp1 opp2) (x : X) : paths (opp2 x (rigunel1_is is)) (rigunel1_is is) := pr2 (pr2 (pr1 is)) x.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions