proposition: Lemma Qle_mult_nonpos_nonneg : forall x y : Q, Qle x Zero -> Qle Zero y -> Qle (Qmult x y) Zero.
proof: Proof. intros [| x| x] [| y| y] Hx Hy; trivial; try QltCleanAbsurdCases; simpl in |- *; intro H_; inversion H_. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)