proposition: Lemma fbbijK : {in U, cancel (fbbij V) (fbbij U)}.
proof: Proof. Proof using HcardEq. move=> x Hx. have : index (fbbij V x) (enum (fiber V (fbfun x))) = index x (enum (fiber U (fbfun x))). rewrite index_uniq //; last exact: enum_uniq. by rewrite -cardE -HcardEq cardE index_mem mem_enum; apply: mem_fiber. rewrite /fbbij (equi_fbbij Hx) => ->. apply nth_index. by rewrite mem_enum; apply: mem_fiber. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype finset)