proposition: Lemma hqgth_hqneq : ∏ x y : hq, x > y -> hqneq x y.
proof: Proof. intros x y Hlt Heq. rewrite Heq in Hlt. now apply isirreflhqgth with y. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.NumberSystems.RationalNumbers UniMath.Algebra.Archimedean