proposition: Lemma infinitePidgeonHolePrinicple : forall (X:Type) (l:list X) (P:nat -> X -> Prop), (forall n, existsC X (fun x => ~~In x l /\ P n x)) -> existsC X (fun x => In x l /\ forall n, existsC nat (fun m => (n <= m)%nat /\ (P m x))).
proof: Proof. intros X l. induction l; intros P HP G. apply (HP O). intros x [Hx _]. auto with *. apply (G a). split; auto with *. intros n Hn. set (P':= fun m => P (m+n)%nat). assert (HP' : forall m : nat, existsC X (fun x => ~~In x l /\ P' m x)). intros m. unfold P'. destruct (HP (m + n)%nat) as [HG | y [Hy0 Hy1]] using existsC_ind. apply existsC_stable; auto. apply existsWeaken. exists y. split; auto. revert Hy0. cut (In y (a :: l) -> In y l);[tauto|]. intros Hy0. destruct Hy0; auto. elim (Hn (m + n)%nat). rewrite H. auto with *. destruct (IHl P' HP') as [HG | x [Hx0 Hx1]] using existsC_ind. tauto. apply (G x). split; auto with *. unfold P' in Hx1. intros n0. destruct (Hx1 n0) as [HG | m [Hm0 Hm1]] using existsC_ind. apply existsC_stable; auto. apply existsWeaken. exists (m + n)%nat. split; auto. auto with *. Qed.
imports: CoRN.stdlib_omissions.List