Take the 2-minute tour ×  I am trying to write an induction
hypothesis specifically for proving properties of even numbers.
I formulated and proved the following:  Theorem
ind_hyp_on_evens: forall (p : nat -> Prop),  (p 0 -> (forall n,
p n -> p (S (S n))) ->  forall n, p (n + n)).  intros p P0 P1.
intro n. assert(p (n + n) /\ p (S (S (n + n)))).  induction n as
[| n'].   split. unfold plus. assumption. unfold plus.  apply
(P1 0). destruct IHn' as [A B].  rewrite <- plus_Snm_nSm.
rewrite -> ? plus_Sn_m. rewrite <- plus_Snm_nSm. rewrite -> ?
plus_Sn_m. apply (P1 (S (S (n' + n')))). destruct H as [H1 H2].
assumption. Qed.   Despite the fact that it's proved, any
attempt to use it results in the error message: "Error: Not the
right number of induction arguments."  Can someone please tell
me what is the problem with the induction hypothesis, or
otherwise, how to apply it??    share|improve this question How
did you attempt to apply it? Post your code that led to the
error message. –  Gilles May 12 '12 at 21:56 add