proposition: Lemma Zsucc_Qplus (z: Z): inject_Z (Z.succ z) = inject_Z z + 1.
proof: Proof. apply Zplus_Qplus. 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