proposition: Lemma inject_Z_nonneg (z: Z): (0 <= z)%Z -> 0 <= inject_Z z.
proof: Proof. Proof with auto. intro. change (inject_Z 0 <= inject_Z z). rewrite <- Zle_Qle. assumption. 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