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