proposition: Lemma Qnum_nonneg (x : Q) : (0 <= Qnum x)%Z <-> (0 <= x)%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