proposition: Lemma powerset_not_product x y z: powerset x <> y \times z.
proof: Proof. move => eq1. move:(setP_0i x); rewrite eq1 => /setX_pair. rewrite /pairp kpairE /kpair_def;set t := singleton _ => h. have /in_set0 //: inc t emptyset by rewrite - h; apply:set2_1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)