proposition: Theorem Qcmult_integral : forall x y, x*y=0 -> x=0 \/ y=0.
proof: Proof. intros. destruct (Qmult_integral x y); try qc; auto. injection H as [= H]. rewrite <- (Qred_correct (x*y)). rewrite <- (Qred_correct 0). rewrite H; auto with qarith. Qed.
imports: Field QArith Znumtheory Eqdep_dec