proposition: Lemma Qmult_lt_0_compat : forall a b : Q, 0 < a -> 0 < b -> 0 < a * b.
proof: Proof. intros a b Ha Hb. destruct a,b. unfold Qlt, Qmult, QArith_base.Qnum, QArith_base.Qden in *. rewrite Pos2Z.inj_mul. rewrite Z.mul_0_l, Z.mul_1_r in *. apply Z.mul_pos_pos; assumption. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool