小编Mat*_*chi的帖子

基本上,我想证明以下结果:

Lemma nat_ind_2 (P: nat -> Prop): P 0 -> P 1 -> (forall n, P n -> P (2+n)) ->
    forall n, P n.

这就是所谓的双重归纳的复发方案.

我试图证明它应用感应两次,但我不确定我会以这种方式得到它.实际上,我在那时陷入困境:

Proof.
  intros. elim n.
    exact H.
    intros. elim n0.
      exact H0.
      intros. apply (H1 n1).