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