proposition: Lemma Qmult_Qdiv_pos_Qle: forall x y z t : Q, Zero < z -> Zero < t -> 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_pos_pos | stepl (x*t); [ stepr (y*z) | idtac]; trivial; field; apply Qlt_not_eq ]; trivial. Qed.