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