Some Remarks

• Induction on nat in the proof of :

   mult2_even : forall n:nat, even (mult2 n).
  

• Induction on (even n) in the proof of :

  sum_even :forall n p:nat, even n -> even p -> even (n + p).
  
  square_even : forall n:nat, even n -> even (n * n).