proposition: Lemma finite_is_maximal_inclusion x: finite_set x <-> (forall y, sub y (\Po x) -> nonempty y -> exists2 z, inc z y & forall t, inc t y -> sub z t -> z = t).
proof: Proof. split. move: x; apply: finite_set_induction0. move=> y yp0 [t ty]. have yp1: forall v, inc v y -> v = emptyset. by move=> v vy; move: (yp0 _ vy); rewrite setP_0 => /set1_P. by ex_tac => v vy tv; rewrite (yp1 _ ty) (yp1 _ vy). move=> a b hrec nba y yp yne. set Z:= Zo y (fun z => inc b z); case: (emptyset_dichot Z) => ze. have yp1: sub y (\Po a). move => t ty; move: (yp _ ty) => /setP_P ta; apply /setP_P => u ut. move: (ta _ ut); case /setU1_P => // ub;empty_tac1 t;apply: Zo_i =>//; ue. by apply: hrec. set T:= fun_image Z (intersection2 a). have Tp: sub T (\Po a). move => t /funI_P [z zZ ->]; apply /setP_P;apply: subsetI2l. have neT:nonempty T. move: ze => [z zZ]; exists (a \cap z); apply /funI_P; ex_tac. move: (hrec _ Tp neT)=> [z zT zm]. move: zT => /funI_P[u uZ iau]. move: uZ => /Zo_P [uy bu]. ex_tac; move=> t ty ut. have bt: inc b t by apply: ut. have tz: inc t Z by apply: Zo_i => //. have it: inc (a \cap t) T by apply /funI_P; ex_tac. have it1: sub z (a \cap t). rewrite iau => w /setI2_P [p1 p2]; apply /setI2_P;split;fprops. move: (zm _ it it1) => zi. apply: extensionality => // v vt; move: (yp _ ty). move /setP_P => tt;move:(tt _ vt); case /setU1_P; last by move => ->. by move => va;apply: (@setI2_2 a);rewrite- iau zi; apply:setI2_i. move=> h. set F := (finite_subsets x). have p1:sub F (\Po x) by apply: Zo_S. have p2: nonempty F. exists emptyset; apply:Zo_i; [ apply: setP_0i| apply:emptyset_finite]. move: (h _ p1 p2) => [z /Zo_P [] /setP_P zpo zf zp]. case: (emptyset_dichot (x -s z)) => ce. have -> //: x = z by apply:extensionality => //; apply:empty_setC. move: ce => [y] /setC_P [yx nyz]. set (t:= z +s1 y). have tF: inc t F. by apply:Zo_i; [apply /setP_P; apply: setU1_sub | apply:setU1_finite]. have zt: sub z t by move=> u uz; rewrite /t; fprops. move: (zp _ tF zt) => tz; case: nyz; rewrite tz /t; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)