proposition: Lemma mem_fiber (S : fibered_set) x : x \in S -> x \in fiber S (fbfun x).
proof: Proof. Proof using. move=> Hx; apply/imsetP; exists x => //. by rewrite inE Hx /=. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype finset)