fact: Definition DivRig_isrinv: ∏ (x : F) (Hx : x != 0), x * / (x,, Hx) = 1 := isDivRig_isrinv (DivRig_isDivRig F).
imports: UniMath.Foundations.Sets UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.MoreFoundations.Tactics