diff --git a/theories/finite.v b/theories/finite.v
index b2fa877ec8c197ec723e734a3823c8bb8e9d7b4c..b18ca5033e997524ac89a5024238d8aeb9be9d93 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.