proposition: Theorem next_P_k_correct : forall k delta, forall P : nat -> Prop, P delta -> (forall x, x < k -> P (kth_S delta x)) -> next_P_k k delta P.
proof: Proof. induction k. intros. simpl. exact H. intros. simpl. split. apply H0. auto with arith. apply IHk. exact H. intros. apply H0. auto with arith. Qed.
imports: PeanoNat Compare