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