Lemma hqone_neq_hqzero : 1%hq != 0%hq. Proof. intro contr. assert (contr_hz : intpart 1%hq != intpart 0%hq). { unfold intpart. apply hzone_neg_hzzero. } apply contr_hz. apply maponpaths, contr. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.RigsAndRings.