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