proposition: Lemma Qmult_Qdiv_pos:forall x y z t: Q, Zero < z*t -> x*t < y*z -> x/z < y/t.
proof: Proof. intros x y z t Hzt Hxyzt; generalize (Qlt_not_eq _ _ Hzt); intro H_zt_nonzero; unfold Qdiv; apply Qdiv_Qmult_pos; [ stepr (Qinv (z*t)); [apply Qinv_pos; assumption|field]; split | unfold Qdiv; repeat rewrite Qinv_involutive; trivial ]; solve[apply Qmult_absorb_nonzero_r with z; trivial] || apply Qmult_absorb_nonzero_l with t; trivial. Qed.