proposition: Lemma Qmult_inj_r (x y z: Q): ~ z == 0 -> (x * z == y * z <-> x == y).
proof: Proof. intro z_ne_0. split; intro E. - rewrite <- (Qmult_1_r x), <- (Qmult_1_r y). rewrite <- (Qmult_inv_r z); auto. do 2 rewrite Qmult_assoc. rewrite E. reflexivity. - rewrite E. reflexivity. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool