fact: Definition DivRig_isrunit_one: ∏ x : F, x * 1 = x := isDivRig_isrunit_x1 (DivRig_isDivRig F).
imports: UniMath.Foundations.Sets UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.MoreFoundations.Tactics