proposition: Lemma infinitePidgeonHolePrinicpleB : forall (X:Type) (l:list X) (f:nat -> X), (forall n, In (f n) l) -> existsC X (fun x => In x l /\ forall n, existsC nat (fun m => (n <= m)%nat /\ (f m)=x)).
proof: Proof. intros X l f H. apply infinitePidgeonHolePrinicple. intros n. apply existsWeaken. exists (f n). auto with *. Qed.
imports: CoRN.stdlib_omissions.List