proposition: Theorem Kmult_integral_contrapositive: forall x y, x <> 0 -> y <> 0 -> x * y <> 0.
proof: Proof. intros x y H H1 H2. case (Kmult_integral H2); auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith