proposition: Lemma finite_powerset x: finite_set x -> finite_set (\Po x).
proof: Proof. move=> fsx. set (t:= Zo (\Po x) (fun a=> finite_set (\Po a))). suff fspt: (finite_subsets_prop x t). move: (finite_subsets_pr x)=> [p1 p2]. move: (p2 _ fspt) => aux. have:(inc x t). apply: aux; apply: Zo_i =>//;apply: setP_Ti. by move /Zo_P; case. split. rewrite /t; apply: Zo_i; first by apply /setP_P;fprops. rewrite setP_0; apply: set1_finite. move=> z X zx =>/Zo_P [] /setP_P Xx fspX; apply: Zo_i. by apply /setP_P; apply setU1_sub. case: (inc_or_not z X); first by move => zX; rewrite setU1_eq. move=> nzX. set (w:= fun_image (\Po X) (fun t => t +s1 z)). have eq: (equipotent (\Po X) w). set (f:= Lf (fun t => t +s1 z) (\Po X) w). have ta: (lf_axiom (fun t => t +s1 z) (\Po X) w). move=> u => uX; apply /funI_P; exists u => //. have ff: (function f) by rewrite /f;apply: lf_function. exists f; split. split;rewrite /f. apply: lf_injective=>//; move => u v /setP_P uX /setP_P vX sv. set_extens x1 => xs. have: (inc x1 (u +s1 z)) by fprops. rewrite sv; case /setU1_P=>//; move=> h; case: nzX; apply: uX; ue. have: (inc x1 (v +s1 z)) by fprops. rewrite - sv; case /setU1_P=>//; move=> h; case: nzX; apply: vX; ue. apply: lf_surjective=>//. by move=> y => /funI_P. by rewrite /f; aw. by rewrite /f; aw. have ->: (\Po (X +s1 z)= (\Po X) \cup w). set_extens u. move /setP_P => sut; apply /setU2_P. case: (inc_or_not z u) => h. right;apply /funI_P; exists (X \cap u). apply /setP_P => //; apply: subsetI2l. set_extens v. move => vu; move: (sut _ vu); case /setU1_P; last by move => ->; fprops. move => vx;apply /setU1_P; left; fprops. by case /setU1_P; [ move =>/setI2_P [] | move => -> ]. left; apply /setP_P;move=> v vu; move: (sut _ vu); case /setU1_P => //. move=> vz; case: h; ue. case /setU2_P. move => /setP_P h; apply /setP_P => v vu; fprops. move => /funI_P [x1 wX ->]; apply /setP_P => v; case /setU1_P => h. by apply /setU1_P; left; move/setP_P: wX; apply. rewrite h; fprops. apply: finite_union2=>//. have aux: (cardinal (\Po X) = cardinal w) by apply /card_eqP. by red; rewrite -aux. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)