proposition: Lemma isarchring_isarchCF {X : ConstructiveField} (R : hrel X) : isarchring R -> isarchCF R.
proof: Proof. intros H. intros x. apply (isarchring_2 R H x). 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