proposition: Lemma hq0lehandplus: ∏ n m : hq, 0 <= n -> 0 <= m -> 0 <= (n + m).
proof: Proof. intros n m Hn Hm. eapply istranshqleh, hqlehandplusl, Hm. now rewrite hqplusr0. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.NumberSystems.RationalNumbers UniMath.Algebra.Archimedean