proposition: Lemma nat_triple_ind : forall P : nat -> Prop, P 0 -> P 1 -> P 2-> (forall n, P n -> P(S (S (S n)))) -> forall n, P n.
proof: Proof. intros P H0 H1 H2 Hind. apply nat_k_ind with 2. compute. split. exact H2. split. exact H1. exact H0. exact Hind. Qed.
imports: PeanoNat Compare