Lemma hq0leminus : ∏ r q : hq, r <= q -> 0 <= q - r. Proof. intros r q Hr. apply hqlehandplusrinv with r. unfold hqminus. rewrite hqplusassoc, hqlminus. now rewrite hqplusl0, hqplusr0. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics.