proposition: Lemma nds_fL_prop2 f m (q:= (fL f) +c m) : inc f (permutations n) -> natp m -> q <c n -> (forall j, j<c m -> pL f ((fL f) +c j)) -> [\/ (m = n -c k /\ forall j, j <c n -> q <=c j -> pS f j), pL f q | q <> \0c /\ exists p, [/\ natp p, csucc (q +c p) <c n, pL f (csucc (q +c p)), pL f (cpred q) & forall z, z <=c p -> pS f (q +c z) ]].
proof: Proof. move => fp mN inb Hi. move: (nds_fL_prop fp) => [sa _ sb sc sd]. move/permutationsP: fp => [bf sf tf]. have ff: function f by fct_tac. have qN: natp q by apply: NS_sum. have kN:= (NS_lt_nat kln nN). set E1 := Zo Nat (fun z => [/\ z <c n, pL f z & q <=c z]). set E2:= Zo Nat (fun z => [/\ z <c n, pL f z & z <c q]). set E3:= n -s k. have: disjoint E1 E2. by apply: disjoint_pr => u /Zo_P[_ [_ _ ha]]/Zo_P[_ [_ _ /(cleNgt ha)]]. move/csum2_pr5;rewrite - csum2cl - csum2cr. have E3tf: sub E3 (target f) by rewrite tf;move => t /setC_P []. have ->: E1 \cup E2 = fun_image E3 (Vf (inverse_fun f)). set_extens t => h. have[ha hb]: t <c n /\ k <=c Vf f t by case/setU2_P:h => /Zo_P[_ [ha hb _]]. have tsf: inc t (source f) by rewrite sf; apply /(NltP nN). have se:=(inverse_V2 bf tsf). apply/funI_P; exists (Vf f t); last by exact. apply /setC_P; split; [ Wtac | by move/(NltP kN) => /(cleNgt hb)]. move/funI_P:h => [z zi ->]; move: (E3tf _ zi) => ft. have eq2:=(inverse_V bf ft). have zt:= (inverse_Vis bf ft). rewrite sf in zt; move /(NltP nN): zt => lt1. have izN:= (NS_lt_nat lt1 nN). move/setC_P: zi => [/(NS_inc_nat nN) zN hb]. case: (NleT_el kN zN) => zz; last by case: hb; apply /(NltP kN). by case: (NleT_el qN izN) => lea; apply /setU2_P; [left | right]; apply:Zo_i => //; split => //; rewrite /pL eq2. have ->: E2 = fun_image m (fun z => (fL f) +c z). set_extens t. move/Zo_P => [tN [tn h tq]]; apply/funI_P. case: (cleT_el (proj31_1 sb)(proj31_1 tq)) => le1. move:tq; rewrite - (cdiff_pr le1) => tq. move /(NltP mN):(csum_lt2l sa (NS_diff (fL f) tN) mN tq) => di; ex_tac. by move: h (sd _ le1);rewrite /pL /pS => ua /(cleNgt ua). move /funI_P => [z /(NltP mN) zi ->]; apply/Zo_P. have lt1:= (clt_ltT (csum_Meqlt sa zi) inb). have sf1 := (csum_Meqlt sa zi). split; [ exact:(NS_lt_nat lt1 nN) | by split => //; apply: Hi ]. rewrite cardinal_fun_image; last first. by move => i j /E3tf /(inverse_V bf) {2}<- /E3tf /(inverse_V bf) {2}<- ->. rewrite cardinal_fun_image; last first. by move => i j im jm /=; apply:(csum_eq2l sa); apply: (NS_inc_nat mN). rewrite /E3 -/(_ -c _) (card_card (CS_nat mN)) => cc. have cE1N: natp (cardinal E1). by move:(NS_diff k nN); rewrite cc => /(NS_in_suml (CS_cardinal E1)). have ci:= (CS_nat mN). case: (cleT_ell (CS_diff n k) ci) => cink. + constructor 1; split; first by symmetry. move => j ljn lqj. have jsf: inc j (source f) by rewrite sf; apply /(NltP nN). move:(Vf_target ff jsf); rewrite tf; move/(NltP nN) => ha. case: (cleT_el (proj31_1 kln) (proj31_1 ha)) => hb; last exact. rewrite cink - {1} (csum0l ci) in cc. move:(esym(csum_eq2r mN NS0 cE1N cc))=>/card_nonempty hw. have jE1: inc j E1 by apply:Zo_i; [apply: (NS_lt_nat ljn nN) | ]. empty_tac1 j. + by move: (csum_M0le (cardinal E1) ci);rewrite csumC - cc=> /(cltNge cink). + have lt1: Vf f q <c n by apply/(NltP nN); Wtac; rewrite sf;apply/(NltP nN). case: (cleT_el (CS_nat kN) (proj31_1 lt1)) => lt2; first by constructor 2. constructor 3. case: (equal_or_not m \0c) => inz. by move:sc lt2; rewrite /pL /q inz (csum0r (proj31_1 sb))=> ua /(cleNgt ua). split; first by move/csum_nz; case. case: (emptyset_dichot E1) => nee. by move: (proj2 cink); rewrite cc nee cardinal_set0 (csum0l ci). have seB: sub E1 Nat by apply:Zo_S. move: (inf_Nat seB nee) =>[]; set j:= intersection E1 => ja jb. move/Zo_P: ja => [jN [ljn jc lqj]]. have eq0:= (cdiff_pr lqj). case: (equal_or_not (j -c q) \0c) => eq1. by move: jc; rewrite - eq0 eq1 (csum0r (proj31 lqj)) /pL => /(cltNge lt2). move: (cpred_pr (NS_diff _ jN) eq1)=> []. set p := (cpred (j -c q)) => pN pv. have eq4:q +c csucc p = j by rewrite - pv. have eq2: csucc (q +c p) = j by rewrite - (csum_nS _ pN). move: (cpred_pr mN inz) => [ia ib]. have eq3: q = csucc (fL f +c (cpred m)) by rewrite -(csum_nS _ ia) - ib. move: (cpred_pr1 (CS_sum2 (fL f) (cpred m))); rewrite - eq3 => eq5. move: (cltS ia); rewrite - ib => /Hi; rewrite - eq5 => eq6. exists p; rewrite eq2; split => //. move => z /(cltSleP pN) zm. move:(csum_Meqlt qN zm); rewrite eq4 => l1. have ra := (clt_ltT l1 ljn). have qnz:= (NS_lt_nat ra nN). move/(NltP nN):(ra); rewrite - sf => /(Vf_target ff); rewrite tf. move /(NltP nN) => /proj31_1 fzn. case: (cleT_el (CS_nat kN) fzn) => // l2. have: (inc (q +c z) E1). by apply:Zo_i => //; split => //; apply:(Nsum_M0le _ qN). by move/jb => /(cltNge l1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)