Lemma fldchoice0_right {X : fld} (e : X) (neq : (e != 0)%ring): (fldchoice0 e) = inr neq. Proof. apply isapropdec, setproperty. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.RigsAndRings.