fact: Definition isDivRig (X : rig) : UU := isnonzerorig X × (∏ x : X, x != 0%rig -> multinvpair X x).
imports: UniMath.Foundations.Sets UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.MoreFoundations.Tactics