Lemma hq0lehandplus: ∏ n m : hq, 0 <= n -> 0 <= m -> 0 <= (n + m). Proof. intros n m Hn Hm. eapply istranshqleh, hqlehandplusl, Hm. now rewrite hqplusr0. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics.