Lemma hq0lehandmult: ∏ n m : hq, 0 <= n -> 0 <= m -> 0 <= n * m. Proof. intros n m. exact hqmultgeh0geh0. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics.