Lemma isarchfld_isarchring {X : fld} (R : hrel X) : ∏ (Hadd : isbinophrel (X := rigaddabmonoid X) R) ( Hmult : isringmultgt X R) (Hirr : isirrefl R), isarchfld R → isarchring R. Proof. intros Hadd Hmult Hirr H. split. - intros x Hx. case (fldchoice x) ; intros x'. + generalize (H (pr1 x')). apply hinhfun. intros n. exists (pr1 n). abstract (pattern (1%ring : X) at 1 ; rewrite <- (pr1 (pr2 x')) ; apply (isringmultgttoisrringmultgt _ Hadd Hmult _ _ _ Hx (pr2 n))). + apply hinhpr. exists O. abstract (apply fromempty ; refine (Hirr _ _) ; rewrite x' in Hx ; apply Hx). - exact H. Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.DivisionRig. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.ConstructiveStructures. Require Import UniMath.MoreFoundations.Tactics.