proposition: Lemma Qlt_mult_neg_pos : forall x y : Q, Qlt x Zero -> Qlt Zero y -> Qlt (Qmult x y) Zero.
proof: Proof. intros [| x| x] [| y| y] Hx Hy; trivial; simpl in |- *; auto with *; [ inversion Hx | inversion Hy ]. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)