proposition: Lemma nat2_ind (P: nat -> Prop): P 0 -> P 1 -> (forall n, P n -> P (n.+2)) -> forall n, P n.
proof: Proof. move=> H0 H1 H n. suff: (P n /\ P (n.+1)) by case. by elim: n=>//n; case=> H2 H3; split=>//; last by apply: H. Qed.
imports: mathcomp(ssreflect eqtype ssrnat ssrbool ssrfun seq)