proposition: Lemma Qdiv_Qmult_pos:forall x y z t: Q, Zero < z*t -> x/z < y/t -> x*t < y*z.
proof: Proof. abstract (intros x y z t Hzt Hxyzt; stepl (z*t*(x/z)); [stepr (z*t*(y/t)) | idtac]; [apply (Qlt_reg_mult_pos_l (z*t) (x/z) (y/t) Hzt Hxyzt) | field | field ]; [ apply Qmult_absorb_nonzero_r with z | apply Qmult_absorb_nonzero_l with t ]; apply Qlt_not_eq; assumption). Qed.