proposition: Theorem EvenNOdd : forall n : Z, Even n -> ~ Odd n.
proof: Proof. intros n H1; red in |- *; intros H2; case H1; case H2; intros z1 Hz1 z2 Hz2. absurd (n = n); auto. pattern n at 1 in |- *; rewrite Hz1; rewrite Hz2; repeat rewrite (fun x => Zplus_comm x 1). case z1; case z2; simpl in |- *; try (intros; red in |- *; intros; discriminate). intros p p0; case p0; simpl in |- *; try (intros; red in |- *; intros; discriminate). Qed.
imports: Reals ZArith List PeanoNat Psatz