fact: Definition CommDivRig_iscomm_mult: ∏ x y : F, x * y = y * x := rigcomm2 (pr1 F).
imports: UniMath.Foundations.Sets UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.MoreFoundations.Tactics