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