proposition: Theorem next_P_k_complete : forall k delta P, next_P_k k delta P -> P delta /\ (forall x, x < k -> P (kth_S delta x)).
proof: Proof. induction k. intros. split. simpl in H. auto. intros. inversion H0. intros. assert (P delta /\ forall x, x<k -> P(kth_S delta x)). apply IHk. apply next_P_k_strong. auto. split. destruct H0. auto. intros. apply le_le_S_eq in H1. destruct H1. apply H0. auto with arith. apply eq_add_S in H1. rewrite H1. simpl in H. destruct H. apply H. Qed.
imports: PeanoNat Compare