proposition: Lemma Zmult_ab0a0b0 : forall a b : Z, (a * b)%Z = 0%Z -> a = 0%Z \/ b = 0%Z.
proof: Proof. simple induction a. simpl in |- *. left. reflexivity. intro p. simple induction b. simpl in |- *. right. reflexivity. simpl in |- *. intros. discriminate H. simpl in |- *. intros. discriminate H. intro. simple induction b. simpl in |- *. right. reflexivity. simpl in |- *. intros. discriminate H. simpl in |- *. intros. discriminate H. Qed.
imports: ZArith EqNat