proposition: Lemma Qmult_resp_Qle_neg_r: forall t x y : Q, t < Zero -> x * t <= y * t -> 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 (x*t)); apply Qle_lt_trans with (y*t); trivial; apply Qlt_reg_mult_neg_r; assumption. Qed.