proposition: Lemma Qmult_resp_Qlt_neg_l: forall t x y : Q, t < Zero -> t * x < t * y -> y < x.
proof: Proof. intros t x y Ht Hxt; destruct (Qtrichotomy_inf x y) as [[Hxy|Hxy]|Hxy]; trivial; contradiction (Qlt_irreflexive (t*x)); [ apply Qlt_transitive with (t*y); trivial; apply Qlt_reg_mult_neg_l | rewrite <- Hxy in Hxt] ; trivial. Qed.