proposition: Lemma finite_surj A `{Finite A} B `{Finite B} : 0 < card A ≤ card B → ∃ g : B → A, Surj (=) g.
proof: Proof. intros [??]. destruct (finite_inhabited A) as [x']; auto with lia. exists (λ y : B, default x' (decode_nat (encode_nat y))). intros x. destruct (encode_decode B (encode_nat x)) as (y&Hy1&Hy2). { pose proof (encode_lt_card x); lia. } exists y. by rewrite Hy2, decode_encode_nat. Qed.
imports: stdpp(options)