proposition: Lemma Sperner_9 C (F := Vf (inverse_fun (Lf cardinal C (csucc n)))) (xi := fun i => union (F (csucc i) -s (F i))): inc C Sperner_mx_chain -> forall i, i<c n -> F (csucc i) = (F i) +s1 (xi i).
proof: Proof. move => Cm. move: (Sperner_8 Cm) => Ha. move:Cm => /Zo_P[ha hb]. move:ha=> /total_subordersP [qa qb]. move:(subp_osr E) Sperner_p0 => [or sr] nN. have Xig i j: i <=c n -> j <=c n -> i <=c j -> sub (F i) (F j). move => lin ljn lij. move: (Ha _ lin) (Ha _ ljn)=> [ra rb] [rc rd]. move: (proj2 qb (F i) (F j)); rewrite iorder_sr // => h. case:(h ra rc) => /iorder_gle1/sub_gleP/proj33 //. by move/sub_smaller; rewrite rb rd => ji; rewrite (cleA ji lij). have rec A B: sub A B /\ singletonp (B -s A) -> B = A +s1 (union (B -s A) ). by move => [sab [t tv]]; rewrite - {1} (setU2_Cr sab) tv setU_1. move => i lin; apply: rec. move: (NS_lt_nat lin nN) => iN. move/(cleSltP iN): (lin) => sin. move: (Xig i (csucc i) (proj1 lin) sin (cleS iN)) => sii. split => //; apply /set_of_card_oneP. move:(Ha _ (proj1 lin)) (Ha _ sin) => [_ rc] [_ rd]. have fsX:finite_set (F (csucc i)) by apply/NatP; rewrite rd; fprops. by rewrite(cardinal_setC4 sii fsX) rc rd (Nsucc_rw iN) csumC(cdiff_pr1 NS1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)