proposition: Lemma Qlt_reg_mult_neg_l: forall x y z : Q, x < Zero -> y < z -> x * z < x * y.
proof: Proof. intros x y z Hx Hyz; apply Qlt_Zero_Qminus_neg; stepl (x*(z-y)); try ring; apply Qlt_mult_neg_pos; trivial; apply Qlt_Qminus_Zero; assumption. Qed.