proposition: Lemma Sperner_17 U V: sub U V -> sub V E -> exists2 C, inc C Sperner_mx_chain & (inc U C /\ inc V C).
proof: Proof. move => sUV sVE. move:(sub_smaller sUV) (sub_smaller sVE). set a := cardinal U; set b := cardinal V; rewrite -/n => leab lebn. have lean := cleT leab lebn. have nN:= Sperner_p0. have sUE := (sub_trans sUV sVE). suff: exists g, [/\ bijection_prop g n E, Vfs g a = U & Vfs g b = V]. move => [g [gA gB gC]]; move: (Sperner_5 gA). move/(NleP nN): lebn => p1; move/(NleP nN): lean => p2. move => Fp; ex_tac; split; apply/funI_P; [ ex_tac | by exists b]. move: (Sperner_16 sUE) => [ga [bga sga tga] ga2]. pose U1 := V -s U; pose V1 := E -s V. have suE: sub U1 E by move => t /setC_P [/sVE]. have svE: sub V1 E by move => t /setC_P []. have fsU: natp(cardinal U1). apply/card_finite_setP;exact: (sub_finite_set suE fsE). have fsV: natp(cardinal V1). apply/card_finite_setP;exact: (sub_finite_set svE fsE). have duv1: disjoint U1 V1 by apply: disjoint_pr => x /setC_P [xv _]/setC_P[_ ]. move: (Sperner_15 fsU fsV duv1) => [gb]. have eqa: (U1 \cup V1) = E -s U. set_extens t. case/setU2_P => /setC_P [ta tb]; apply/setC_P; split; fprops. move => /setC_P [tE tU]; case: (inc_or_not t V) => tv. by apply: setU2_1; apply/setC_P. by apply: setU2_2; apply/setC_P. have ->: (cardinal U1 +c cardinal V1) = n -c a. rewrite csum2cl csum2cr -(csum2_pr5 duv1) eqa cardinal_setC4 //. rewrite eqa => -[bgb sgb tgb] g2p. pose h x := Yo (x <c a) (Vf ga x) (Vf gb (x -c a)). have fga: function ga by fct_tac. have fgb: function gb by fct_tac. have aN := NS_le_nat lean nN. have san := (proj33 lean). have sbn := (proj33 lebn). have bN := NS_le_nat lebn nN. have ax: lf_axiom h n E. rewrite /h => i iin; move:(NS_inc_nat nN iin) => iN. case: (NleT_el aN iN) => cia; last by Ytac0; Wtac. move/(NltP nN): iin => lin. rewrite (Y_false (cleNgt cia)). have: inc (i -c a) (source gb). rewrite sgb; apply/(NltP (NS_diff a nN)); apply: (cdiff_pr7 cia lin nN). by move/ (Vf_target fgb); rewrite tgb => /setC_P;case. have ha: sub (cardinal U) (source ga) by ue. have he y: inc y U -> exists2 i, inc i a & y = h i. rewrite - ga2; move/(Vf_image_P fga ha) => [i ia ->]; ex_tac. by rewrite /h Y_true //; apply/NltP. have bgp: bijection_prop (Lf h n E) n E. saw;apply: bijective_if_same_finite_c_surj; aw. rewrite card_card //; fprops. by apply: finite_set_nat. apply: (lf_surjective ax) => y yE; case: (inc_or_not y U) => yU. move/he:yU =>[i ia ->]; exists i => //; apply: (san _ ia). have: inc y (target gb) by rewrite tgb; apply/setC_P. move/(proj2 (proj2 bgb)) =>[i]; rewrite sgb => id ->. move: (NS_inc_nat (NS_diff a nN) id) => iN. move/(NltP (NS_diff a nN)): id => lin. exists (i +c a). apply/(NltP nN). by move:(csum_Mlteq aN lin); rewrite -{2}(cdiff_pr lean)(csumC a). by rewrite /h (Y_false (cleNgt(csum_Mle0 i (CS_nat aN)))) cdiff_pr1. set gc := (Lf h n E). move: (bgp) => [bgc sgc tgc]; move: (proj1 (proj1 bgc)) => fgc. have hd i : inc i a -> inc (Vf ga i) U. move => ia; rewrite - ga2; apply/(Vf_image_P fga ha); ex_tac. have hb: Vfs gc a = U. have sa:sub a (source (Lf h n E)) by ue. set_extens t. move/(Vf_image_P fgc sa) => [u ua ->]; move: (san _ ua) => un. by rewrite /h LfV // Y_true; [ apply: hd | apply/NltP]. move => /he [i ia ->]; apply/(Vf_image_P fgc sa); ex_tac. by move: (san _ ia) => un; rewrite LfV. have hc: Vfs gc b = V. have sb:sub b (source (Lf h n E)) by ue. have cu1: cardinal U1 = b -c a. by rewrite (cardinal_setC4 sUV) //; apply: (sub_finite_set sVE). have aux: (b -c a) <=c (n -c a). apply:(csum_le2l aN (NS_diff a bN) (NS_diff a nN)). by rewrite (cdiff_pr leab)(cdiff_pr lean). have sb1: sub (cardinal U1) (source gb). by rewrite sgb cu1; apply: (proj33 aux). set_extens t. move/(Vf_image_P fgc sb) => [u ub ->]; move: (sbn _ ub) => un;rewrite LfV//. rewrite /h; move: (NS_inc_nat bN ub)=> uN; case: (NleT_el aN uN) => cia. have sub1v: sub U1 V by move => v /setC_P []. rewrite (Y_false (cleNgt cia)); apply: sub1v; rewrite - g2p. apply/(Vf_image_P fgb sb1); exists (u -c a) => //; rewrite cu1. apply/(NltP (NS_diff a bN)). apply:(csum_lt2l aN (NS_diff a uN) (NS_diff a bN)). by rewrite (cdiff_pr leab)(cdiff_pr cia); apply/NltP. by Ytac0; apply: sUV; apply: hd; apply /NltP. move => tV; apply/(Vf_image_P fgc sb); case: (inc_or_not t U) => tU. by move /he:tU=> [i ia ->]; exists i;[apply: (proj33 leab)| rewrite LfV//; apply: san]. have: inc t U1 by apply/setC_P. rewrite - g2p => /(Vf_image_P fgb sb1) [u uab ->]. rewrite cu1 in uab. have uN:= NS_inc_nat (NS_diff a bN) uab. have ua2: u <c b -c a by apply/(NltP (NS_diff a bN)). have ua3: inc (u +c a) b. by apply /(NltP bN); rewrite- (cdiff_pr leab) csumC; apply:csum_Meqlt. have ua4: inc (u +c a) n by apply: sbn. by ex_tac; rewrite LfV// /h(Y_false (cleNgt(csum_Mle0 u (CS_nat aN)))) cdiff_pr1. by exists gc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)