proposition: Lemma prl_ne2_prop1 i: inc i (psI S) -> (prl_ne1_condii i <-> prl_ne1_condii' i).
proof: Proof. move => iI. split => hb. move=> F fa fb fc fd; apply:hb => // A AF fsA /nonemptyP neA. have hc: forall B, finite_set B -> sub B F -> B = emptyset \/ exists2 z, inc z F & sub z (intersection B). apply: finite_set_induction; first by move => _; left. move => a b h1 h2; right. have bu:= (setU1_1 a b); have bF := (h2 _ bu). have be: nonempty (a +s1 b) by ex_tac. case:(h1 (sub_trans (@subsetU2l _ _) h2)) => h3. by rewrite h3 set0_U2 setI_1; exists b. move: h3 =>[z zF zi1]; move: (fd _ _ bF zF) => [t [tf ta tb]]; ex_tac. move => x xt; apply/(setI_P be) => y /setU1_P; case => hc. exact:(setI_hi (zi1 _ (tb _ xt)) hc). by rewrite hc; apply: ta. case: (hc _ fsA AF) => // [] [z zF zi]. case: (emptyset_dichot z) => ze; first by case:fc; ue. by move:ze =>[zz ziz]; exists zz; apply: zi. move => F fa fb fc. set G := fun_image(Zo (\Po F) (fun z => finite_set z /\ nonempty z)) intersection. have pg1 A: finite_set A -> nonempty A -> sub A F -> inc (intersection A) G. move => pa pb pc; apply/funI_P; exists A => //; apply/Zo_P; split => //. by apply /setP_P. have pg2: sub F G. move => t tf; rewrite - (setI_1 t); apply: pg1. - by apply: set1_finite. - fprops. - by apply: set1_sub. have neG: nonempty G by case:fb => [x xf]; exists x; apply: pg2. suff: nonempty (intersection G). by move => [x /(setI_P neG) xp]; exists x; apply/(setI_P fb) => t /pg2/xp. apply:hb. - move => t /funI_P [z /Zo_P[/setP_P zF] [fz nez] ->]. exact:(FS_inter iI (sub_trans zF fa) nez). - done. - move => /funI_P [z /Zo_P[/setP_P zF] [fz nez] xv]. by move/nonemptyP: (fc _ zF fz nez); rewrite xv. - move => x y /funI_P[xa /Zo_P[/setP_P xF] [fx nex] xv] /funI_P[ya /Zo_P[/setP_P yF] [fy ney] yv]. have ne1: nonempty (xa \cup ya) by case:nex => [a ax]; exists a; fprops. set z := intersection(xa \cup ya); exists z; split => //. + by apply: pg1; [ apply: finite_U2 | | apply:setU2_12S]. + rewrite xv;move => t /(setI_P ne1) h; apply/(setI_P nex) => k ka. apply:h; fprops. + rewrite yv;move => t /(setI_P ne1) h; apply/(setI_P ney) => k ka. apply:h; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)