proposition: Lemma fbbijP (U V : fibered_set) : (forall i, #|fiber U i| = #|fiber V i|) -> [/\ {in U &, injective (fbbij V)}, [set fbbij V x | x in U] = V & {in U, forall x, fbfun (fbbij V x) = fbfun x} ].
proof: Proof. Proof using. move=> HcardEq. split; [exact: can_in_inj (fbbijK _) | | exact: equi_fbbij]. rewrite -setP => y. apply/imsetP/idP => [[x Hx] ->{y} | Hy]; first exact: fbset_fbbij. by exists (fbbij U y); [exact: fbset_fbbij | rewrite fbbijK]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype finset)