proposition: Lemma fbbij_in_fiber x : x \in U -> fbbij V x \in fiber V (fbfun x).
proof: Proof. Proof using HcardEq. move=> Hx; rewrite -mem_enum; apply mem_nth. by rewrite -cardE -HcardEq cardE index_mem mem_enum; apply: mem_fiber. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype finset)