fact: Definition DivRig_isassoc_mult: ∏ x y z : F, x * y * z = x * (y * z) := isDivRig_isassoc_mult (DivRig_isDivRig F).
imports: UniMath.Foundations.Sets UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.MoreFoundations.Tactics