proposition: Lemma fldchoice0_left {X : fld} (e : X) (eq : (e = 0)%ring): (fldchoice0 e) = inl eq.
proof: Proof. apply isapropdec, setproperty. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Maybe UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Domains_and_Fields UniMath.Algebra.RigsAndRings