proposition: Lemma Qle_nat (n: nat): 0 <= inject_Z (Z_of_nat n).
proof: Proof. rewrite <- (Zle_Qle 0). apply Zle_0_nat. 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