proposition: Lemma Qmult_injective_l (z: Q) (Znz: ~ z == 0): forall x y, (x * z == y * z <-> x == y).
proof: Proof. split; intro E. rewrite <- (Qmult_1_r x). rewrite <- (Qmult_1_r y). rewrite <- (Qmult_inv_r _ Znz). do 2 rewrite Qmult_assoc. rewrite E. reflexivity. rewrite E. 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