Lemma hztohqandlth': ∏ n m : hz, (hztohq n < hztohq m)%hq -> hzlth n m. Proof. intros n m Hlt. apply neghzgehtolth. intro Hle. apply hztohqandgeh in Hle. apply hqgehtoneghqlth in Hle. apply Hle. exact Hlt. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics.