proposition: Lemma nat_pigeonhole (f : nat → nat) (n1 n2 : nat) : n2 < n1 → (∀ i, i < n1 → f i < n2) → ∃ i1 i2, i1 < i2 < n1 ∧ f i1 = f i2.
proof: Proof. intros Hn Hf. pose (f' (i : fin n1) := nat_to_fin (Hf _ (fin_to_nat_lt i))). destruct (finite_pigeonhole f') as (i1&i2&Hi&Hf'); [by rewrite !fin_card|]. apply (not_inj (f:=fin_to_nat)) in Hi. apply (f_equal fin_to_nat) in Hf'. unfold f' in Hf'. rewrite !fin_to_nat_to_fin in Hf'. pose proof (fin_to_nat_lt i1); pose proof (fin_to_nat_lt i2). destruct (decide (i1 < i2)); [exists i1, i2|exists i2, i1]; lia. Qed.
imports: stdpp(options)