Lemma fldchoice0 {X : fld} (e : X) : coprod (e = 0%ring) (e != 0%ring). Proof. destruct (fldchoice e) as [ x_inv | x_0 ]. - right. apply isnonzerofromrinvel. { apply nonzeroax. } exact x_inv. - left; assumption. 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.