proposition: Lemma nds_fL_prop f: inc f (permutations n) -> [/\ natp (fL f), (fL f) <=c k, (fL f) <c n, pL f (fL f) & forall j, j <c (fL f) -> pS f j].
proof: Proof. move => fp; rewrite /fL; set E:= Zo _ _. move/permutationsP:(fp) =>[[injf [ff fs]] sf tf]. have nee: nonempty E. move:(perm_int_surj nN fp kln) => [i lin si]. exists i;apply:Zo_i;[ by apply: (NS_lt_nat lin nN) | split => //]. rewrite /pL si; apply: (cleR (proj31_1 kln)). have seN: sub E Nat by apply:Zo_S. move: (inf_Nat seN nee); set i:= intersection E. move => [/Zo_P [iN [ha hb]] etc]. have kN:= (NS_lt_nat kln nN). have aux: forall j, j <c i -> pS f j. move => j lji. move: (clt_ltT lji ha) => ljn; move/(NltP nN): (ljn) => jb. have /(NltP nN) /proj31_1 cf: (inc (Vf f j) n) by Wtac. case: (cleT_el (proj31_1 kln) cf) => // jfL; case:(cltNge lji). by apply: etc; apply:(Zo_i (NS_lt_nat ljn nN)). split => //. case: (NleT_el iN kN) => // lki. have aux2: forall i, i <=c k -> pS f i. by move => j jk; apply: aux; exact: (cle_ltT jk lki). rewrite /pS in aux2. have h3: sub (Nintc k) (source f). move => j/(NintcP kN) ja; rewrite sf; apply/(NltP nN);exact:(cle_ltT ja kln). have su1: sub (Vfs f (Nintc k)) k. move => t /(Vf_image_P ff h3) [u /(NintcP kN) ul1 ->]. by apply/(NltP kN); apply: aux2. move: (sub_smaller su1). rewrite(cardinal_image h3 injf) (card_Nintc kN) (card_nat kN) => l1. case: (cleNgt l1 (cltS kN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)