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