proposition: Lemma Qmult_Qdiv_neg_Qle:forall x y z t : Q, z<Zero -> t<Zero -> x * t<=y * z -> x / z <= y / t.
proof: Proof. intros x y z t Hz Ht Hxyzt; apply Qmult_resp_Qle_pos_r with (z*t). apply Qlt_mult_neg_neg; trivial. stepl (x*t); [ stepr (y*z) |]; trivial; field; auto. Qed.