fact: Definition isConstrDivRig (X : rig) (R : tightap X) := isnonzeroCR X R × (∏ x : X, R x 0%rig -> multinvpair X x).
imports: UniMath.Algebra.DivisionRig UniMath.Algebra.Domains_and_Fields UniMath.Algebra.Apartness UniMath.MoreFoundations.Tactics