Definition afldfracapart : apart ( commringfrac A (aintdomazerosubmonoid A)). Proof. intros. unfold apart. split with afldfracapartrel. exact isapartafldfracapartrel. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields.