proposition: Lemma Sperner_10 C (F := Vf (inverse_fun (Lf cardinal C (csucc n)))) (g := Lf (fun i => union (F (csucc i) -s (F i))) n E): inc C Sperner_mx_chain -> bijection_prop g n E /\ C = chain_of_fun g.
proof: Proof. move => Cm. move:(subp_osr E) Sperner_p0 => [or sr] nN. move: (Sperner_8 Cm) (Sperner_9 Cm); rewrite -/F => Ha Hb. move: (Sperner_7 Cm) =>[ax card_b]. move:Cm => /Zo_P[ha hb]. move:ha=> /total_subordersP [qa qb]. pose xi i := union (F (csucc i) -s F i). have Xie i: i <c n -> inc (xi i) (F (csucc i)) by move/Hb ->; fprops. have axg: lf_axiom xi n E. move => i /(NltP nN) lin; move: (Xie _ lin) (NS_lt_nat lin nN)=> in1 iN. by move/(cleSltP iN): lin => /Ha/proj1 /qa; rewrite sr; move/setP_P; apply. have Xif i j: i <c j -> j <=c n -> inc (xi i) (F j). move => lij ljn. move:(NS_le_nat ljn nN) => jN. move:(NS_lt_nat lij jN) => iN. move: (Xie _ (clt_leT lij ljn)) => h. move/(cleSltP iN): lij => lij. move: (Ha _ (cleT lij ljn)) (Ha _ ljn) => [ra rb] [rc rd]. move: (proj2 qb (F (csucc i)) (F j)); rewrite iorder_sr // => hyp. case:(hyp ra rc) => /iorder_gle1/sub_gleP/proj33; first by apply. by move/sub_smaller; rewrite rb rd => ji; rewrite (cleA ji lij). have Xih i: i <c n -> ~inc (xi i) (F i). move => lin xx; move: (f_equal cardinal (Hb i lin)); rewrite (setU1_eq xx). move: (NS_lt_nat lin nN) => iN. rewrite (proj2(Ha i (proj1 lin))). move/(cleSltP iN): lin => /Ha/proj2 ->. exact: (nesym (proj2 (cltS iN))). have bgp: bijection_prop g n E. rewrite /g;saw;apply: bijective_if_same_finite_c_inj; aw. - by rewrite /n double_cardinal. - by apply: finite_set_nat. - apply: lf_injective => // i j /(NltP nN) lin /(NltP nN) ljn => sxi. move: (NS_lt_nat lin nN) (NS_lt_nat ljn nN) => iN jN. case: (NleT_ell iN jN) => // lij. by case: (Xih j ljn); move: (Xif i j lij (proj1 ljn)); rewrite /xi sxi. by case: (Xih i lin); move: (Xif j i lij (proj1 lin)); rewrite /xi - sxi. move: (bgp) => [[injg [fg sjg]] sg tg]. have Xik i: i <=c n -> Vfs g i = F i. move => lin; move:(NS_le_nat lin nN) => iN. have sig: sub i (source g) by rewrite sg; exact: (proj33 lin). move: (proj2 (Ha _ lin)) => c1. have fs1: (finite_set (F i)) by apply /NatP; rewrite c1. have sa: sub (Vfs g i) (F i). move => t /(Vf_image_P fg sig) [u /(NltP iN) ui ->]; rewrite/g LfV//. by apply: Xif. by apply/(NltP nN); apply: (clt_leT ui lin). apply: (cardinal_setC5 fs1 sa). by rewrite c1 (cardinal_image sig injg) card_nat. split => //;set_extens t. move => tC. have tc: inc t (source (Lf cardinal C (csucc n))) by aw. move: (Vf_target (proj1(proj1 card_b)) tc); aw => lin. move/(NleP nN): (lin) => liin. by apply/funI_P; ex_tac;rewrite (Xik _ liin) - {1} (inverse_V2 card_b tc); aw. move=>/funI_P [i /(NleP nN) lin ->]; rewrite (Xik _ lin). exact: (proj1 (Ha _ lin)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)