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