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