About Even Numbers

Show that the double of any natural number is even, then show that the square of any even number is even too.
Show that every even natural number is the double of some natural number.
You must use the following definitions :

Require Import Arith.

Inductive even : nat -> Prop :=
  | O_even : even 0
  | plus_2_even : forall n:nat, even n -> even (S (S n)).


Hint Resolve O_even plus_2_even.

Fixpoint mult2 (n:nat) : nat :=
  match n with
  | O => 0
  | S p => S (S (mult2 p))
  end.

Solution

This file

Remarks and/or hints