proposition: Lemma finite_pigeonhole `{Finite A} `{Finite B} (f : A → B) : card B < card A → ∃ x1 x2, x1 ≠ x2 ∧ f x1 = f x2.
proof: 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.
imports: stdpp(options)