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