proposition: 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: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.Domains_and_Fields UniMath.Algebra.ConstructiveStructures UniMath.MoreFoundations.Tactics