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))
Remarks and/or hints