test2.v

Require Import ZArith_base.
Require Import ZArith.BinInt.
Require Import Omega.

Local Open Scope Z.

Definition Even (x : Z) := exists (k : Z), x = 2*k.
Definition Odd (x : Z) := exists (k : Z), x = 2*k + 1.

Theorem even_plus_even : forall (x y : Z), Even x -> Even y -> Even (x + y).
Proof.
  unfold Even.
  intros until 0.
  intros [k] [k'].
  exists (k + k').
  omega.
Qed.

Theorem even_plus_odd : forall (x y : Z), Even x -> Odd y -> Odd (x + y).
Proof.
  unfold Even, Odd.
  intros until 0.
  intros [k] [k'].
  exists (k + k').
  omega.
Qed.

Theorem odd_plus_odd : forall (x y : Z), Odd x -> Odd y -> Even (x + y).
Proof.
  unfold Even.
  intros until 0.
  intros [k] [k'].
  exists (k' + k + 1).
  omega.
Qed.