Lemma isarchhq : isarchfld (X := hq) hqgth. Proof. simple refine (isarchfldfrac hzintdom _ _ _ _ _ _ _ _). - exact isirreflhzgth. - exact istranshzgth. - apply isarchhz. Qed.
Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.