fact: Definition isDivRig_mult {X : rig} (is : isDivRig X) : binop X := λ x y : X, (x * y)%rig.
imports: UniMath.Foundations.Sets UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.MoreFoundations.Tactics