proposition: Lemma hztohqandleh': ∏ n m : hz, (hztohq n <= hztohq m)%hq → hzleh n m.
proof: Proof. intros n m Hle Hlt. simple refine (Hle _). apply hztohqandgth. exact Hlt. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.NumberSystems.RationalNumbers UniMath.Algebra.Archimedean