proposition: Lemma fpowersetS A B : (fpowerset A `<=` fpowerset B) = (A `<=` B).
proof: Proof. apply/fsubsetP/fsubsetP => [sub_pA_pB a|subAB X]. by have := sub_pA_pB [fset a]; rewrite !fpowersetE !fsub1set. by rewrite !fpowersetE => /fsubsetP XA; apply/fsubsetP => x /XA /subAB. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)