proposition: Lemma next_P_k_strong2 : forall k delta P, next_P_k (S k) delta P -> next_P_k k (S delta) P.
proof: Proof. induction k. intros. unfold next_P_k. fold next_P_k. unfold next_P_k in H. rewrite kth_S_special in H. destruct H. exact H. intros. unfold next_P_k. fold next_P_k. split. unfold next_P_k in H. fold next_P_k in H. unfold kth_S. fold kth_S. destruct H. rewrite kth_S_sym in H. unfold kth_S in H. fold kth_S in H. rewrite kth_S_sym in H. exact H. apply IHk. unfold next_P_k in H. fold next_P_k in H. destruct H. exact H0. Qed.
imports: PeanoNat Compare