proposition: Lemma Qlt_Qmult_cancel_r: forall x y z : Q, Zero < x -> y * x< z * x -> y < z.
proof: Proof. intros x y z Hx Hxy; apply Qlt_Zero_Qminus; apply Qsgn_9; transitivity (Zmult (Qsgn x) (Qsgn (z-y))); [ rewrite (Qsgn_7 _ Hx); auto with zarith | rewrite <- Qsgn_15; apply Qsgn_7; stepr (z*x - y*x); try ring; apply Qlt_Qminus_Zero; trivial ]. Qed.