proposition: Theorem nat_k_ind : forall k P, next_P_k k 0 P -> (forall n, P n -> P(kth_S k n)) -> forall n, P n.
proof: Proof. intros. assert (forall n:nat, next_P_k (S k) n P). apply nat_ind. unfold next_P_k. fold next_P_k. split. unfold kth_S. assert (kth_S k 0=S k). apply kth_S_special. rewrite <- H1. apply H0. apply next_P_k_special with k. exact H. exact H. intros. unfold next_P_k. fold next_P_k. split. rewrite kth_S_sym. apply H0. apply next_P_k_strong2 in H1. apply next_P_k_special with k. exact H1. apply next_P_k_strong2. exact H1. destruct H1 with n. fold next_P_k in H3. apply next_P_k_special with k. exact H3. Qed.
imports: PeanoNat Compare