proposition: Lemma Qmult_injective_r (z: Q) (Znz: ~ z == 0): forall x y, (z * x == z * y <-> x == y).
proof: Proof. intros. do 2 rewrite (Qmult_comm z). apply Qmult_injective_l. 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