Definition hqgth : hrel hq := fldfracgt hzintdom isdeceqhz isplushrelhzgth isringmulthzgth ( ct ( hzgth , isdecrelhzgth, 1%hz , 0%hz ) ) hzneqchoice .
Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.