proposition: Lemma equi_fbbij x : x \in U -> fbfun (fbbij V x) = fbfun x.
proof: Proof. Proof using HcardEq. move=> /fbbij_in_fiber. by move=> /imsetP[im0]; rewrite inE => /andP[_ /eqP <-] ->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype finset)