proposition: Lemma Sperner_5 g: bijection_prop g n E -> inc (chain_of_fun g) Sperner_mx_chain.
proof: Proof. move => [ [[fg ing] sjg] sg tg]. move:(subp_osr E) Sperner_p0 => [or sr] nN. have H i: i <=c n -> sub i (source g) by move/proj33; rewrite sg. have pa : {inc (csucc n) &, injective (Vfs g)}. move => i j /(NleP nN) lin /(NleP nN) ljn ss. move: (NS_le_nat lin nN)(NS_le_nat ljn nN) => iN jN. move: (H _ lin) (H _ ljn) => isg jsg. case: (NleT_ell iN jN) => // lt1. have ij: inc i j by apply/NltP. have: inc (Vf g i) (Vfs g j) by apply/(Vf_image_P fg jsg); ex_tac. rewrite - ss => /(Vf_image_P fg isg) [k ki kv]. move: (ing i k (jsg _ ij) (isg _ ki) kv) => eik. by move/(NltP iN): ki =>/proj2; rewrite eik; case. have ij: inc j i by apply/NltP. have: inc (Vf g j) (Vfs g i) by apply/(Vf_image_P fg isg); ex_tac. rewrite ss => /(Vf_image_P fg jsg) [k ki kv]. move: (ing j k (isg _ ij) (jsg _ ki) kv) => eik. by move/(NltP jN): ki =>/proj2; rewrite eik; case. have aux k: k <=c n -> sub (Vfs g k) E. move => skn; move: (H _ skn) => s1. move => t /(Vf_image_P fg s1) [u uk ->]; Wtac. have sC: sub (chain_of_fun g) (substrate (subp_order E)). by rewrite sr=> t /funI_P [i /(NleP nN) lin ->]; apply/setP_P; apply: aux. apply: Zo_i; last by rewrite(cardinal_fun_image pa) card_card; fprops. apply:(total_suborder_prop or sC). move => x y /funI_P [i /(NleP nN) lin ->] /funI_P [j /(NleP nN) ljn ->]. move: (aux _ lin) (aux _ ljn)=> iA iB. move: (H _ lin) (H _ ljn) => isg jsg. case: (cleT_ee (proj31 lin) (proj31 ljn)) => cij; [left | right]. apply/subp_gleP; split => // t /(Vf_image_P fg isg) [u ui ->]. by apply/(Vf_image_P fg jsg); exists u => //; apply: (proj33 cij). apply/subp_gleP; split => // t /(Vf_image_P fg jsg) [u ui ->]. by apply/(Vf_image_P fg isg); exists u => //; apply: (proj33 cij). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)