proposition: Lemma nds_fL_prop4 f: inc f (permutations n) -> exists g, [/\ inc g (permutations n), nds_sc X n f = nds_sc X n g, fL f = fL g & forall i, i<c n -c k -> pL g ((fL g) +c i) ].
proof: Proof. move => fp. move: (NS_diff k nN) (cleR (CS_diff n k)). move:{1 2 4} (n -c k); apply: Nat_induction. by move => _; exists f; split => // i /clt0. move => q qN Hrec le1. move:(cleS qN) => le2. move: (Hrec (cleT le2 le1)) => [g [ga gb gc gd]]. move: (nds_fL_prop ga) => [aa ab ac ad ae]. have kN:= (NS_lt_nat kln nN). move: (csum_Meqlt kN (clt_leT (cltS qN) le1)). rewrite (cdiff_pr (proj1 kln))=> lt2. move: (cle_ltT (csum_Mleeq q ab) lt2) => lt3. case:(nds_fL_prop2 ga qN lt3 gd). + by move => [ua _]; move: le1 (cltS qN); rewrite - ua => sa /(cleNgt sa). + move => h; exists g; split; [ exact | exact| exact | ]. move => j; move/(cltSleP qN) => ljq. case: (equal_or_not j q) => ejq; [ ue | by apply: gd]. set q1:= fL g +c q. move => [q1p [ j [jN ja jb jc jd]]]. move: (cpred_pr (NS_sum aa qN) q1p); rewrite -/q1; move=> [je ef]. have eg:=(csum_Sn j je). have sa: csucc (csucc (cpred q1 +c j)) <c n by rewrite -eg - ef. have sc: pL g (csucc (csucc (cpred q1 +c j))) by rewrite -eg - ef. have sb: (forall j0, j0 <=c j -> pS g (csucc (cpred q1 +c j0))). by move => j1 jl1; rewrite -(csum_Sn _ je) - ef; apply: jd. move:(nds_fL_prop3 ga je jN sa jc sb sc) => [g1 [r1 r2 r3 r4]]. rewrite -ef in r3 r4. have sw: fL g = fL g1. move: (nds_fL_prop r1) => [aa' _ _ ad' ae']. have af: fL g <=c q1 by apply /csum_M0le; fprops. have q1N: natp q1 by move:(NS_succ je); rewrite - ef. case: (NleT_el aa' q1N) => ag; last first. by move:(ae' _ ag) r4; rewrite /pS/pL => l1 /(cltNge l1). case:(NleT_ell aa aa') => l3. + exact. + move: (ae' _ l3) ad; rewrite /pL/pS (r3 _ (clt_leT l3 ag)). move => l1 l2; case: (cltNge l1 l2). + move: (ae _ l3) ad'; rewrite /pL/pS (r3 _ (clt_leT l3 af)). move => l1 l2;case: (cltNge l1 l2). exists g1;split; [exact | ue| by rewrite gc | ]. move => i /(cltSleP qN) isa; rewrite - sw. case:(equal_or_not i q) => eqi; first by rewrite eqi. move: (csum_Meqlt aa (conj isa eqi));rewrite /pL => /r3 <-. apply: (gd _ (conj isa eqi)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)