proposition: Lemma nat_ind_2: forall P: nat -> Prop, P 0 -> P 1 -> (forall n, P n -> P ((S (S n)))) -> forall n, P n.
proof: Proof. intros P H0 H1 HSS. assert (G: forall m, P m /\ P (S m)). induction m. split; assumption. destruct IHm as [IHm IHSm]. split. assumption. apply (HSS m), IHm. intro n. destruct (G n). assumption. Qed.
imports: List PeanoNat common comparisons