fact: Definition isDivRig_DivRig {X : rig} : isDivRig X -> DivRig := λ is : isDivRig X, X ,, is.
imports: UniMath.Foundations.Sets UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.MoreFoundations.Tactics