proposition: Lemma fpowersetE A B : (B \in fpowerset A) = (B `<=` A).
proof: Proof. apply/imfsetP/fsubsetP => /= [[Z _ -> y /in_fset_valP [] //]|/fsubsetP subYX]. exists (fsub _ B); last by rewrite fsubK. by rewrite powersetE /= -fsubT subset_fsub ?fsubset_refl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)