proposition: Lemma powerset1 x : powerset [set x] = [set set0; [set x]].
proof: Proof. by apply/setP=> A; rewrite inE subset1 orbC set1.unlock !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)