proposition: Lemma hq0leminus : ∏ r q : hq, r <= q -> 0 <= q - r.
proof: Proof. intros r q Hr. apply hqlehandplusrinv with r. unfold hqminus. rewrite hqplusassoc, hqlminus. now rewrite hqplusl0, hqplusr0. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.NumberSystems.RationalNumbers UniMath.Algebra.Archimedean