この講義の「演習として残した」補題に行き詰まっています。こんなふうになります：
Lemma even_double : forall n, even n -> exists k, n = 2 * k.
Proof.
intros n H.
induction H.
...
even次のように定義された帰納的述語はどこにありますか。
Inductive even : nat -> Prop :=
| even0 : even 0
| evenS : forall p:nat, even p -> even (S (S p).
助けてください？私はいつも(S (S p) = 2または似たようなものになります。
編集
私が使用したいくつかの補題と戦術 (完全な証明ではありません):
destruct IHeven
exists (S x)
rewrite mult_succ_l
apply eq_S
apply plus_n_Sm