proposition: Lemma next_P_k_strong : forall k delta P, next_P_k (S k) delta P -> next_P_k k delta P.
proof: Proof. induction k. intros. unfold next_P_k. unfold next_P_k in H. destruct H. exact H0. intros. unfold next_P_k. fold next_P_k. unfold next_P_k in H. fold next_P_k in H. destruct H. destruct H0. split. exact H0. exact H1. Qed.
imports: PeanoNat Compare