proposition: Lemma finite_bijective A `{Finite A} B `{Finite B} : card A = card B ↔ ∃ f : A → B, Inj (=) (=) f ∧ Surj (=) f.
proof: Proof. split. - intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia. exists f; split; [done|]. by apply finite_inj_surj. - intros (f&?&?). apply (anti_symm (≤)); apply finite_inj. + by exists f. + destruct (surj_cancel f) as (g&?). exists g. apply cancel_inj. Qed.
imports: stdpp(options)