proposition: Lemma Qnum_nonpos (x : Q) : (Qnum x <= 0)%Z <-> (x <= 0)%Q.
proof: Proof. destruct x as [n d]. unfold Qle. simpl. now rewrite Zmult_1_r. Qed.
imports: Coq.QArith.QArith Coq.ZArith.ZArith Coq.NArith.NArith Coq.QArith.Qpower Coq.QArith.Qround Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.List