proposition: Theorem Kmult_integral: forall x y, x * y = 0 -> x = 0 \/ y = 0.
proof: Proof. intros x y H. generalize (Eth.(is_zero_correct) x); case (is_zero x); intros (H1, H2); auto; right. apply trans_equal with ((/x) * (x * y)); try field. intros H3; assert (H4 := H2 H3); discriminate. rewrite H; ring. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith