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