proposition: Lemma Qcmult_lt_compat_r : forall x y z, 0 < z -> x < y -> x*z < y*z.
proof: Proof. unfold Qcmult, Qclt; intros; simpl in *. rewrite !Qred_correct in *. eapply Qmult_lt_compat_r; eauto. Qed.
imports: Field QArith Znumtheory Eqdep_dec