proposition: Lemma Qle_mult_nonneg_nonneg : forall x y : Q, Qle Zero x -> Qle Zero y -> Qle Zero (Qmult x y).
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)