proposition: Lemma finite_inj A `{Finite A} B `{Finite B} : card A ≤ card B ↔ ∃ f : A → B, Inj (=) (=) f.
proof: Proof. split. - intros. destruct (decide (card A = 0)) as [HA|?]. { exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). } destruct (finite_surj A B) as (g&?); auto with lia. destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj. - intros [f ?]. unfold card. rewrite <-(fmap_length f). by apply submseteq_length, (finite_inj_submseteq f). Qed.
imports: stdpp(options)