proposition: Lemma nds_fL_prop5 f: inc f (permutations n) -> exists K s1 s2, [/\ sub K k, inc s1 (permutations (cardinal K)), inc s2 (permutations (n -c k)) & nds_sc X n f = nds_sc (fun z => X (k +c z)) (n-c k) s2 +o nds_sc_Ktau X K s1].
proof: Proof. move/nds_fL_prop4 => [g [gp -> _ p1]]; rewrite /nds_sc_Ktau. move:(nds_fL_prop gp) => [qN p2 p3 p4 p5]. move/permutationsP:gp =>[[injg [fg sjg]] sg tg]. rewrite sg tg in sjg. set q := (fL g); rewrite -/q in qN p1 p2 p3 p4 p5. have nkN:=(NS_diff k nN). have le3:=(cdiff_pr3 nN p2 (proj1 kln)). have eq2:=(cdiff_pr (proj1 p3)). have eq3:=(cdiff_pr le3). have eq4:=(cdiff_pr (proj1 kln)). have nqN:= (NS_diff q nN). have qnkN:= (NS_sum qN nkN). have kN:= (NS_lt_nat kln nN). have lt1: q +c (n -c k) <=c n. move: (csum_Mleeq n p2); rewrite - {1} eq4 (csumC k) csumA (csumC _ k). by move/(csum_le2l kN qnkN nN). have sK: sub q (source g) by rewrite sg; exact (proj33 (proj1 p3)). move: (cardinal_image sK injg);set K := Vfs g q. rewrite (card_nat qN) => cK. have iKP: forall i, inc i K <-> exists2 j, inc j q & i = Vf g j. move => i; split; by move /(Vf_image_P fg sK). have h0:sub K k. by move => t /iKP [j jE ->]; apply/(NltP kN); apply: p5; apply/(NltP qN). set E1:= (q +c (n -c k)) -s q. set K1 := Vfs g E1. have sK1: sub E1 (source g). move => t /setC_P [/(NltP qnkN) ha _]; rewrite sg; apply/(NltP nN). exact: (clt_leT ha lt1). have iK1P: forall i, inc i K1 <-> exists2 j, inc j E1 & i = Vf g j. move => i; split; by move /(Vf_image_P fg sK1). have cK1: cardinal K1 = n -c k. move: (cardinal_image sK1 injg); rewrite -/K1. have ha:=(proj33 (Nsum_M0le (n-c k) qN)). rewrite (cardinal_setC4 ha (finite_set_nat qnkN)). by rewrite (card_nat qnkN) (card_nat qN) csumC (cdiff_pr1 nkN qN). have sK1': sub K1 (n -s k). move => t/iK1P [j ja ->]; apply/setC_P; split. by move: (Vf_target fg (sK1 _ ja)); rewrite tg. have jN: natp j by move:(sK1 j ja); rewrite sg => /(NS_inc_nat nN). move/setC_P:ja => [/(NltP qnkN) ja jb]; dneg h. case: (cleT_el (CS_nat qN) (proj31_1 ja)); last by move/(NltP qN). move => le1; move:(cdiff_pr le1) => eqa. rewrite - eqa in ja. have jc := (csum_lt2l qN (NS_diff q jN) nkN ja). move: (p1 _ jc); rewrite eqa /pL => jd. by move/(NltP kN):h => /(cleNgt jd). move: (proj33 (proj1 kln)) (finite_set_nat nN) => s1 fn. move: (sub_finite_set (@sub_setC n k) fn) => ha. have hb: K1 =c n -s k. by rewrite (cardinal_setC4 s1 fn) (card_nat kN) (card_nat nN) cK1. move:(strict_sub_smaller_contra ha sK1' hb) => eq5. clear s1 fn ha hb. have p6: forall i, i<c n -> q +c (n -c k) <=c i -> pS g i. move => i li1 li2; rewrite /pS; ex_middle h. have isn: inc i (source g) by rewrite sg; apply/(NltP nN). have: inc (Vf g i) K1. rewrite eq5; apply/setC_P; split; [Wtac | by move/(NltP kN)]. move/(iK1P) => [j /setC_P [/(NltP qnkN) ja jb] eqa]. have jsg: inc j (source g). by move: (clt_ltT (clt_leT ja li2) li1) => /(NltP nN); rewrite sg. move: ((proj2 injg) i j isn jsg eqa) => eij; rewrite - eij in ja. case: (cltNge ja li2). have sKb: sub K n by move => t /iKP [ u /sK usf ->]; Wtac. have sKN:=(sub_trans sKb (NS_inc_nat nN)). have fsK:=(sub_nat_finite nN sKb). move:(nth_elt_bf sKN fsK) ; set FK:= Lf _ _ _; move => [pa pb]. have sFK: source FK = q by rewrite /FK cK; aw. have tFK: target FK = K by rewrite /FK cK; aw. have ax2: lf_axiom (nth_elt K) q K. move => t /(NltP qN) lt2; move:(lt2); rewrite - cK => lt3. by move:(nth_set7 (NS_lt_nat lt2 qN) sKN lt3) => [/setC_P []]. pose s1' i := (Vf (inverse_fun FK) (Vf g i)). have ax1: lf_axiom s1' q q. move => t ta;rewrite - sFK; apply:(inverse_Vis pa); rewrite tFK. by apply /iKP; exists t. have pc: forall i, inc i q -> Vf FK (s1' i) = Vf g i. move => i iE; rewrite /s1' (inverse_V pa) // tFK; apply/iKP; ex_tac. set s1 := Lf s1' q q . have s1fb: bijection s1. apply:lf_bijective; first by exact. move => u v uE vE eq6. move: (f_equal (Vf FK) eq6); rewrite (pc _ uE) (pc _ vE) => eq7. exact: (proj2 injg _ _ (sK _ uE) (sK _ vE) eq7). rewrite - sFK;move => y ye. move: (Vf_target (proj1(proj1 pa)) ye); rewrite tFK => /iKP [u us eq1]. by rewrite - sFK in us; ex_tac; rewrite /s1'- eq1 (inverse_V2 pa ye). have s1perm: inc s1 (permutations q). apply/permutationsP; rewrite /s1; saw. set Ec:= (n -c k). pose s2' z := (Vf g (q +c z) -c k). have pd1: forall z, z <c n -c k -> inc (q +c z) (source g). move => z zi. move:(csum_Meqlt qN (clt_leT zi le3)). by rewrite eq2 => /(NltP nN);rewrite - sg => ha. have ax3: lf_axiom s2' Ec Ec. move => z /(NltP nkN) zi. move: (Vf_target fg (pd1 _ zi)); rewrite tg => /(NltP nN) lt2. rewrite -/q - cK in lt2. move:(p1 _ zi);rewrite /pL /s2' - cK=> fzi. apply/(NltP nkN); exact(cdiff_pr7 fzi lt2 nN). have pd: forall z, z <c n -c k -> (s2' z) +c k = Vf g (q +c z). move => z /p1;rewrite /pL /s2' - cK=> fzi. by rewrite csumC; apply:cdiff_pr. set s2 := Lf s2' Ec Ec. have s2fb: bijection s2. apply:bijective_if_same_finite_c_inj. + by rewrite /s2; aw. + by rewrite /s2/Ec; aw; apply:finite_set_nat. + apply: lf_injective => // u v /(NltP nkN) ue /(NltP nkN) ve eq. move: (f_equal (fun z => z +c k) eq). rewrite (pd _ ue) (pd _ ve) => eq7. move:(proj2 injg _ _ (pd1 _ ue)(pd1 _ ve) eq7). exact:(csum_eq2l qN (NS_lt_nat ue nkN) (NS_lt_nat ve nkN)). have s2perm: inc s2 (permutations (n -c k)). apply/permutationsP; rewrite /s2; saw. exists K, s1, s2; rewrite cK;split => //. rewrite /nds_sc_Ktau. set X1:= osumf (fun z => X (nth_elt K (Vf s1 z))) q. have r1: X1 = osumf (fun z => X (Vf g z)) q. apply: (osumf_exten qN) => i /(NltP qN) iE. have vK: inc (Vf g i) (target FK) by rewrite tFK;apply/iKP; ex_tac. rewrite /s1/s1' !LfV// -{2} (inverse_V pa vK) {2} /FK cK. rewrite LfV// - sFK; apply: (inverse_Vis pa vK). set X2:= osumf (fun z=> X (Vf g (z +c q))) (n -c k). have r2: X2 = osumf (fun z => X (k +c Vf s2 z)) (n -c k). apply:(osumf_exten nkN). move => z znk /=;rewrite (csumC z) (csumC k) - (pd _ znk) /s2 LfV//. by apply/(NltP nkN). move: Xax => [ [hw _] oe hu hv]. have aX: nds_ax (fun z => X (Vf g z)) n. move => z /(NltP nN) zi. rewrite - sg in zi. by move:(Vf_target fg zi); rewrite tg => /(NltP nN) /hw /proj32_1. have aX2: nds_ax (fun z=> X (Vf g (z +c q))) (n -c q). move=> z zle1; apply: aX; move: (csum_Mlteq qN zle1). by rewrite (csumC (_ -c _)) eq2. rewrite /nds_sc - {1} eq2;rewrite - eq2 in aX. rewrite - eq3 in aX2. rewrite (osum_fA qN nqN aX) -/X1 - r1 - eq3. rewrite (osum_fA nkN (NS_diff (n -c k) nqN) aX2) - r2; congr (_ +o X1). have knz1:= (cdiff_nz kln). move: (cpred_pr nkN knz1) => [nk1N nk1v]. rewrite /X2 nk1v (osum_fS _ nk1N). set X3:= osumf _ _. set X4:= osumf _ _. set a := X _. move:(cltS nk1N); rewrite -nk1v => /p1; rewrite /pL csumC => le1. have lt2: inc ((cpred (n -c k) +c q)) (source g). rewrite csumC;apply/pd1; rewrite {2} nk1v; apply:(cltS nk1N). have lt3: Vf g (cpred (n -c k) +c q) <c n. by apply/(NltP nN); rewrite - {2}tg; Wtac. move: (hw _ lt3) (hv _ le1 lt3); rewrite -/a => ap da. have oa:= proj32_1 ap. have oX4: ordinalp X4. apply:(OS_osumf nk1N) => t ta;apply: aX2. move: (clt_leT ta (cleS nk1N)); rewrite - nk1v => sa. exact: (clt_leT sa (Nsum_M0le ((n -c q) -c (n -c k)) nkN)). set wa:=((n -c q) -c csucc (cpred (n -c k))). have wN: natp wa by rewrite /wa; fprops. have wa1: (wa +c (n -c k)) = (n -c q). by rewrite /wa -nk1v (csumC (_ -c _)) cdiff_pr. have oX3:ordinalp X3. apply:(OS_osumf wN) => z zw;apply: aX2;rewrite eq3. by move: (csum_Mlteq nkN zw); rewrite -nk1v wa1. rewrite (osumA oX3 oa oX4); congr (_ +o X4). rewrite /X3 -/wa - nk1v. have eq7: ((wa +c (n -c k)) +c q) = n by rewrite wa1 csumC eq2//. have: wa +c ((n -c k) +c q) <=c n by rewrite csumA eq7; fprops. clear eq7 wa1. move: wa wN; apply: Nat_induction. by move => _ ; rewrite osum_f0 (osum0l oa). move=> j jN Hrec. have sN:= NS_sum jN (NS_sum nkN qN). rewrite (csum_Sn _ jN) => /(cleSltP sN) ha. have oS: ordinalp (osumf (fun z => X (Vf g ((z +c (n -c k)) +c q))) j). apply:(OS_osumf jN) => z zl; apply:aX2;rewrite eq3. move:(csum_Mlteq nkN zl) => hc. move:(Nsum_M0le (j +c (n -c k)) qN); rewrite csumC => hd. rewrite csumA in ha; move: (cdiff_pr7 hd ha nN). rewrite (cdiff_pr1 (NS_sum jN nkN) qN) => he; exact: (clt_ltT hc he). rewrite (osum_fS _ jN) - csumA. set j0 := j +c ((n -c k) +c q). have j0b: inc j0 (source g) by rewrite sg; apply/(NltP nN). rewrite -/j0 in ha. have hb:q +c (n -c k) <=c j0. rewrite /j0 csumC (csumC j); apply:csum_M0le; fprops. move:(Vf_target fg j0b); rewrite tg => /(NltP nN) => hc. have ofp:= hw _ hc. have oft:= proj32_1 ofp. rewrite - (osumA oft oS oa) (Hrec (proj1 ha)). move: (hu _ (p6 _ ha hb)) => hd. rewrite - hd in da; exact: (ord_negl_p7 ofp ap da). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)