proposition: Lemma Qmult_resp_Qle_neg_l: forall t x y : Q, t < Zero -> t * x <= t * y -> y <= x.
proof: Proof. intros t x y Ht Hxt; case (Q_le_lt_dec y x); trivial; intro Hxy; apply False_ind; apply (Qlt_irreflexive (t*x)); apply Qle_lt_trans with (t*y); trivial; apply Qlt_reg_mult_neg_l; assumption. Qed.