proposition: Lemma inject_Z_injective (a b: Z): inject_Z a = inject_Z b <-> a = b.
proof: Proof. unfold inject_Z. split; congruence. 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