proposition: Lemma hq0lehandmult: ∏ n m : hq, 0 <= n -> 0 <= m -> 0 <= n * m.
proof: Proof. intros n m. exact hqmultgeh0geh0. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.NumberSystems.RationalNumbers UniMath.Algebra.Archimedean