proposition: Lemma Qmult_le_0_compat : forall a b, 0 <= a -> 0 <= b -> 0 <= a*b.
proof: Proof. intros a b Ha Hb. unfold Qle in *. simpl in *. rewrite Z.mul_1_r in *. auto with *. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool