proposition: Lemma hztohqandlth': ∏ n m : hz, (hztohq n < hztohq m)%hq -> hzlth n m.
proof: Proof. intros n m Hlt. apply neghzgehtolth. intro Hle. apply hztohqandgeh in Hle. apply hqgehtoneghqlth in Hle. apply Hle. exact Hlt. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.NumberSystems.RationalNumbers UniMath.Algebra.Archimedean