Lemma hqgth_hqneq : ∏ x y : hq, x > y -> hqneq x y. Proof. intros x y Hlt Heq. rewrite Heq in Hlt. now apply isirreflhqgth with y. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics.