Lemma isarchCF_isarchring {X : ConstructiveField} (R : hrel X) : ∏ (Hadd : isbinophrel (X := rigaddabmonoid X) R) ( Hmult : isringmultgt X R) (Hirr : isirrefl R), (∏ x : X, R x 0%CF → (x ≠ 0)%CF) → isarchCF R → isarchring R. Proof. intros Hadd Hmult Hirr H0 H. split. - intros x Hx. generalize (H (CFinv x (H0 _ Hx))). apply hinhfun. intros (n,Hn). exists n. change 1%ring with (1%CF : X). rewrite <- (islinv_CFinv x (H0 x Hx)). apply isringmultgttoisrringmultgt. exact Hadd. exact Hmult. exact Hx. exact Hn. - 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.