proposition: Lemma not_a_powerset3 x: \3c <> powerset x.
proof: Proof. move => h. have i12: inc \1c \2c by exact: set2_2. have: inc \2c \3c by apply/(NltP NS3); exact: (cltS NS2). rewrite h => /setP_P => h'; move: (h' _ i12) => h''. have : inc (singleton \1c) \3c by rewrite h; apply/setP_P => t /set1_P ->. rewrite /card_three (succ_of_nat NS2) => /setU1_P; case. have hx := (set1_1 \1c). case/set2_P => hy; move: hx; rewrite hy; first by move => /in_set0. by move /set1_P => hz; move:(set1_1 \0c); rewrite -/card_one hz => /in_set0. move => hy. move: (set2_1 \0c \1c). rewrite -/card_two -hy => /set1_P bad. by case: card1_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)