proposition: Lemma Zmult_Qmult (x y: Z): inject_Z (x * y) = inject_Z x * inject_Z y.
proof: Proof. reflexivity. 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