proposition: Theorem Qmult_integral_l : forall x y, ~ x == 0 -> x*y == 0 -> y == 0.
proof: Proof. intros (x1, x2) (y1, y2). unfold Qeq, Qmult; simpl. rewrite !Z.mul_1_r, Z.mul_eq_0. intuition. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool