proposition: Lemma Qcmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x*z <= y*z.
proof: Proof. unfold Qcmult, Qcle; intros; simpl in *. repeat rewrite Qred_correct. apply Qmult_le_compat_r; auto. Qed.
imports: Field QArith Znumtheory Eqdep_dec