proposition: Lemma Sperner_cf14 f (F := fun k => (subsets_with_p_elements k E)): free_rep f -> source f = cn -> oddp n -> target f = F (chalf n) \/ target f = F (csucc (chalf n)).
proof: Proof. move => fp sg on. have hN := NS_half (proj1 on). move: (Sperner_cf11 fp sg) => [Ha Hb]. move: (half_odd on); rewrite /cdouble - csum_nn - (csum_Sn _ hN); set q := chalf n => nv. pose a i := cardinal (Vf f i). have ap i: inc i (source f) -> a i = q \/ a i = csucc q. move => isf; move: (Sperner_cf0 fp isf) => [_ lean aN]. case: (Hb _ isf); [by left | move => eq ; right]. apply:(csum_eq2r hN aN (NS_succ hN)). by move: (cdiff_pr lean); rewrite eq {2} nv. move: (fp) => [[[ffp injp] [_ sj]] cf /Sperner_p4[ste tff]]. case: (p_or_not_p (exists2 i, inc i (source f) & a i = q)); last first. have le1: csucc q <=c n by rewrite nv; apply: csum_M0le; fprops. have le2: is_half_n n (csucc q). right; rewrite {1} nv csumC; apply: cdiff_pr1; fprops. move => bad ; right; apply: (Sperner_cf12 fp sg le1 le2). move => t tf; apply/ Zo_P;split; first by move: (ste _ tf). move: (sj _ tf) =>[k kf ->]. case: (ap _ kf) => // dv. ex_middle bad1; case: bad; ex_tac. have nN := proj1 on. move => [i0 i0sg ai0v]; left. have le1: q <=c n by apply cle_halfn_n. have le2: is_half_n n q by left. apply: (Sperner_cf12 fp sg le1 le2). move => t tf; apply/ Zo_P;split; first by move: (ste _ tf). move: (sj _ tf) =>[k kf kv]; rewrite kv;case: (ap _ kf) => //. rewrite /a - kv => ct. set U := (Vf f i0). have Utf: inc U (target f) by rewrite /U; Wtac. have cU: cardinal U = q by []. have H A p: cardinalp p -> cardinal A = csucc p -> exists B x, [/\ A = B +s1 x, cardinal B = p, sub B A & B <> A]. move => qN cA. case: (emptyset_dichot A) => Ae. by case: (@succ_nz p); rewrite - cA Ae cardinal_set0. move: (rep_i Ae) => rt; exists (A -s1 (rep A)), (rep A). move:(csucc_pr2 rt); rewrite cA. move/ (csucc_inj qN (CS_cardinal _)) => <-. rewrite (setC1_K rt); split => //b; first by move/setC1_P; case. by move: rt; rewrite - {2} b => /setC1_P [_] []. move: (H _ _ (proj31 le1) ct) => [V [x0 [ra cV rv]]]; case. have stE: sub t E by apply/setP_P; apply: ste. have sVE := (sub_trans rv stE). suff tV: (inc V (target f)) by apply: (tff V t tV tf); apply/subp_gleP. have pN: natp (cardinal (V -s U)). by apply/NatP; apply: sub_finite_set fsE => x /setC_P [/sVE]. suff: forall p, natp p -> forall V, sub V E -> cardinal (V -s U) = p -> cardinal V = q -> inc V (target f). by move => hyp; apply: (hyp _ pN V sVE). clear V cV t tf k kf kv ct ra rv sVE stE x0 pN. apply: Nat_induction. have fsU: finite_set U by apply/NatP; rewrite cU. move => V sVE /card_nonempty/empty_setC cdz cvq. by rewrite - cU in cvq; rewrite (cardinal_setC5 fsU cdz cvq). move => p pN Hrec V Ve cvd cvq. move: (H (V -s U) p (CS_nat pN) cvd) => [W [x1 [pa pb pc pd]]]. case: (emptyset_dichot (U -s V)) => nes. have fsV: finite_set V by apply/NatP; rewrite cvq. by rewrite - cvq in cU; rewrite -(cardinal_setC5 fsV (empty_setC nes) cU). move /setC_P: (rep_i nes); set y := rep (U -s V);move =>[yU yV]. have yE: inc y E by move /setP_P: (ste _ Utf); apply. have sW: sub W (V -s U) by rewrite pa => x xW; fprops. move: (setU1_1 W x1); rewrite - pa => /setC_P[x1V x1U]. pose W1 := W \cup (U\cap V). pose V' := W1 +s1 y. case: (inc_or_not x1 W) => ixw. by case: pd; rewrite pa; symmetry;apply:setU1_eq. have eq3: V +s1 y = V' +s1 x1. set_extens z; case/setU1_P. + move => zV; apply/setU1_P. case: (equal_or_not z x1) => zx1; [by right | left; apply/setU1_P]. left;apply/setU2_P; case: (inc_or_not z U) => zU; first by right; fprops. by move:(setC_i zV zU); rewrite pa => /setU1_P; case => zv //; left. + move->; apply: setU1_r; apply:setU1_1. + case/setU1_P; [ case/setU2_P; last move => /setI2_P [] | move ->];fprops. by move => /sW/setC_P [zW _]; apply: setU1_r. + by move ->; apply: setU1_r. have ixV: ~ (inc x1 V'). case/setU1_P; first by case/setU2_P => // /setI2_P [ x1v]; case: x1U. by move => ex1y; case: yV; rewrite - ex1y. have cardV': cardinal V' = q. move: (f_equal cardinal eq3); rewrite (csucc_pr ixV) (csucc_pr yV) - cvq. move => h;symmetry; apply:csucc_inj; fprops. have svE: sub V' E. move => x /setU1_P; case; last by move ->. by case/setU2_P; [ move=> /pc /setC_P [/Ve] | case/setI2_P => _ /Ve ]. have sWE:= (setU1_sub Ve yE). have eq1: V' -s U = W. set_extens x. case/setC_P; case/setU1_P;first by case/setU2_P => // /setI2_P []. by move ->; case. move => xW;move: (sW _ xW) => /setC_P [qa qb]. by apply /setC_P; split => //; apply/setU1_P; left; apply/setU2_P; left. move: pb; rewrite - eq1 => cV'. move:(Hrec V' svE cV' cardV') => V'tf. move: (Sperner_17 (@sub_setU1 V y) sWE) =>[C Cp [i1 i2]]. move: (Ha C Cp) => [j jsf fjC]. move/Zo_S: (Cp) => /Sperner_3 cij. have Wt: inc (Vf f j) (target f) by Wtac. case : (ap _ jsf) => cfj. have xx:V =c Vf f j by ue. by rewrite (cij V (Vf f j) i1 fjC xx). have xx: (V +s1 y) =c Vf f j by rewrite (csucc_pr yV) cvq - cfj. move: Wt; rewrite - (cij _ (Vf f j) i2 fjC xx) eq3 => vtf. have bad: gle r V' (V' +s1 x1) by apply/subp_gleP; split; fprops; ue. case: ixV; rewrite (tff V'(V' +s1 x1) V'tf vtf bad); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)