Lemma hztohqandleh': ∏ n m : hz, (hztohq n <= hztohq m)%hq → hzleh n m. Proof. intros n m Hle Hlt. simple refine (Hle _). apply hztohqandgth. exact Hlt. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics.