From 296f00b95e7c4a322327860d8348ba049d2df5b1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 11 Apr 2022 16:22:44 +0200
Subject: [PATCH] Add Pigeon Hole principle.

---
 theories/finite.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/finite.v b/theories/finite.v
index b2fa877e..b18ca503 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -419,3 +419,11 @@ Section sig_finite.
   Lemma sig_card : card (sig P) = length (filter P (enum A)).
   Proof. by rewrite <-list_filter_sig_filter, fmap_length. Qed.
 End sig_finite.
+
+Lemma finite_pigeon_hole `{Finite A} `{Finite B} (f : A → B) :
+  card B < card A → ∃ x1 x2, x1 ≠ x2 ∧ f x1 = f x2.
+Proof.
+  intros. apply dec_stable; intros Heq.
+  cut (Inj eq eq f); [intros ?%inj_card; lia|].
+  intros x1 x2 ?. apply dec_stable. naive_solver.
+Qed.
-- 
GitLab