Definition afldfracapartrelpre : hrel ( A × aintdomazerosubmonoid A ) := fun ab cd => ( pr1 ab * pr1 ( pr2 cd ) ) # ( pr1 cd * pr1 ( pr2 ab ) ).
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields.