proposition: Theorem pigeonhole : forall m n, m < n -> forall f, (forall i, f i < m) -> { i : nat & { j : nat | i < j < n /\ f i = f j } }.
proof: Proof. cut (forall n f, (forall i, f i < n) -> { i : _ & ((i < S n) * { j | j < i /\ f i = f j })%type }). intros; destruct (H (n-1) f) as [i [Li [j [Lj Hij]]]]; eauto. intros i; specialize (H1 i); lia. exists j, i; intuition lia. destruct n. intros f L; specialize (L 0); exfalso; inversion L. induction n; intros f B. now pose proof conj (B 0) (B 1); exists 1; intuition; exists 0; intuition lia. destruct (bounded_lookup f (f (S (S n))) (S (S n))) as [[i Hi]|J]. now exists (S (S n)); intuition; eauto. assert (Eg: { g : nat -> nat | (forall a, a < S (S n) -> f a < f (S (S n)) -> g a = f a) /\ (forall a, a < S (S n) -> f a > f (S (S n)) -> g a = f a - 1) /\ (forall a, g a < S n)}). set (g := fun a => if Compare_dec.lt_dec a (S (S n)) then if Compare_dec.lt_dec (f a) (f (S (S n))) then f a else f a - 1 else 0); exists g. split; [|split]; intro a; intros; unfold g; destruct (Compare_dec.lt_dec a (S (S n))); destruct (Compare_dec.lt_dec (f a) (f (S (S n)))); lia || auto. now specialize (B (S (S n))); lia. now specialize (B a); lia. destruct Eg as [g [g1 [g2 g3]]]. destruct (IHn g) as [i [Li [j [Lj E]]]]. now intros a; eauto. exists i; intuition eauto; exists j; intuition eauto. assert (D: forall a, f a = f (S (S n)) \/ f a < f (S (S n)) \/ f a > f (S (S n))) by (intro;lia). assert (j < S (S n)) by lia. destruct (D i), (D j); intuition eauto; try solve [exfalso; eapply J; eauto]. rewrite (g1 i) in E; eauto. now rewrite (g1 j) in E; eauto. rewrite (g1 i) in E; eauto. rewrite (g2 j) in E; eauto. lia. rewrite (g2 i) in E; eauto. rewrite (g1 j) in E; eauto. lia. rewrite (g2 i) in E; eauto. rewrite (g2 j) in E; eauto. lia. Defined.
imports: Lia