proposition: Lemma Qmult_inj_l (x y z: Q): ~ z == 0 -> (z * x == z * y <-> x == y).
proof: Proof. rewrite (Qmult_comm z x), (Qmult_comm z y). apply Qmult_inj_r. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool