proposition: Lemma pigeon_hole : forall s l, incl l s -> length l > length s -> exists x : A, occur x l >= 2.
proof: Proof. induction s; simpl; intros. apply False_ind. destruct l. simpl in H0. lia. unfold incl in H. simpl in H. apply (H a). auto. destruct l. apply False_ind. simpl in H0. lia. case (In_dec eq_dec a0 l); intro. ded (in_occur eq_dec i). exists a0. simpl. rewrite eq_delta. lia. case (le_lt_dec (occur a l) 1); intro. ded (incl_cons_l H). clear H. destruct H1. ded (incl_cons_r H1). destruct H2. simpl in H. destruct H. subst a0. contr. ded (in_elim_dec eq_dec H2). do 3 destruct H3. assert (~In a x0). apply (occur_notin eq_dec). rewrite H3, occur_app in l0. simpl in l0. rewrite eq_delta in l0. lia. rewrite H3 in H1. ded (incl_app_elim H1). clear H1. destruct H6. ded (incl_cons_r H1). clear H1. destruct H7. contr. ded (incl_cons_l H6). clear H6. destruct H7. clear H6. ded (incl_cons_r H7). clear H7. destruct H6. contr. set (l' := x ++ a0 :: x0). assert (incl l' s). unfold l'. apply incl_app. exact H1. apply incl_cons. exact H. exact H6. assert (length l' > length s). unfold l'. rewrite length_app. simpl. simpl in H0. rewrite H3, length_app in H0. simpl in H0. lia. ded (IHs l' H7 H8). destruct H9. exists x1. assert (occur x1 (a0::l) = occur x1 l' + delta x1 a). unfold l'. rewrite H3. simpl. rewrite !occur_app. simpl. lia. lia. assert (length l > length s). simpl in H0. lia. ded (IHs l H2 H3). destruct H4. exists x. simpl. lia. exists a. simpl. lia. Qed.
imports: CoLoR(ListUtil NatUtil LogicUtil)