Равенство мощностей двух типов finType с биекцией

Question

У меня два finTypeс биекцией между ними. На данный момент мне нужен тот факт, что у них одинаковый кардинал. Однако я не могу найти ни этой леммы, ни других лемм, с помощью которых можно легко доказать утверждение. Мне кажется, что доказательство не должно быть трудным.

Утверждение:

From mathcomp Require Import ssrfun ssrbool eqtype fintype.
Lemma bij_card_eq (T T' : finType) (f : T -> T') : bijective f -> #|T| = #|T'|.
Proof.
Admitted.

Любая помощь приветствуется!

Answer 1

Вот действительно хорошее доказательство этого факта Кириллом Коэном здесь:

From mathcomp Require Import all_ssreflect.

Section BijCard.

Variables U V : finType.
Variable f : U -> V.

Lemma bij_card : bijective f -> #|U| = #|V|.
Proof.
move=> [g fgK gfK]; rewrite -(card_image (can_inj fgK)).
by apply/eq_card=> x; apply/imageP; exists (g x).
Qed.

End BijCard.