Lemma isapartafldfracapartrel : isapart afldfracapartrel. Proof. intros. split. - apply isirreflquotrel. exact isirreflafldfracapartrelpre. - split. + apply issymmquotrel. exact issymmafldfracapartrelpre. + apply iscotransquotrel. exact iscotransafldfracapartrelpre. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields.