even_plus_even_is_even.v

Require Import Arith.Mult.

Definition is_even (n : nat) : Prop :=
  exists (k : nat), n = 2 * k.

Theorem even_plus_even_is_even :
  forall (n m : nat), is_even n /\ is_even m -> is_even (n + m).
Proof.
  intro n.
  intro m.
  intro H0.
  destruct H0 as [H1 H2].
  destruct H1 as [x0 H3].
  destruct H2 as [x1 H4].
  rewrite H3.
  rewrite H4.
  pose proof mult_plus_distr_l as H5.
  symmetry in H5.
  rewrite H5.
  exists (x0 + x1).
  reflexivity.
Qed.