proposition: Lemma powersetS A B : (powerset A \subset powerset B) = (A \subset B).
proof: Proof. apply/subsetP/idP=> [sAB | sAB C /[!inE]/subset_trans->//]. by rewrite -powersetE sAB // inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)