Definition iscomptofldfrac (X : intdom) (is : isdeceq X) {L : hrel X} (is0 : @isbinophrel X L) (is1 : isringmultgt X L) (is2 : L 1 0) (nc : neqchoice L) (isa : isasymm L) : iscomprelrelfun L (fldfracgt X is is0 is1 is2 nc) (tofldfrac X is).
Require Import UniMath.Algebra.Groups.