proposition: Lemma nds_tg9 (X2:= (fun z => X (k +c z))): nds_sums X n = unionf (nds_tn_S X k) (fun v1 => fun_image (nds_sums X2 (n -c k)) (fun v2 => v2 +o v1)).
proof: Proof. set_extens v. move /nds_fL_prop6 => [v1 [v2 [va vb vc]]]. apply/setUf_P; ex_tac; apply/funI_P; ex_tac. move/setUf_P => [v1 /setUf_P [K /setP_P Kp/funI_P [s1 s1p va]]]. move => /funI_P [v2 /funI_P [s2 s2p ->]] => ->; rewrite va; apply/funI_P. set K' := k -s K. set q := cardinal K. have kN:=(NS_lt_nat kln nN). move:(sub_smaller Kp); rewrite (card_nat kN); rewrite -/q => leqk. have lqn:=(cle_ltT leqk kln). have qN:= NS_lt_nat lqn nN. have nkN:=(NS_diff k nN). have qnN:= (NS_sum qN nkN). have sKN:= (sub_trans Kp (NS_inc_nat kN)). have sK'N: sub K' Nat by exact: (sub_trans (@sub_setC k K) (NS_inc_nat kN)). have cK': cardinal K' = k -c q. by rewrite (cardinal_setC4 Kp (finite_set_nat kN)) (card_nat kN). have qqn:=(Nsum_M0le (n -c k) qN). have kqN:= (NS_diff q kN). have q'N: natp (cardinal K') by rewrite cK'. have knk:= (cdiff_pr (proj1 kln)). set qn := q +c (n -c k); rewrite -/qn in qnN qqn. have qnkq: qn +c (k-c q) = n. by rewrite -knk /qn (csumC q) - csumA (cdiff_pr leqk) csumC. have lqnn: qn <=c n by rewrite - qnkq; apply:(Nsum_M0le _ qnN). have sBkBn:=(proj33 (proj1 kln)). move/permutationsP: (s1p) => [bs1 ss1 ts1]; move: (proj1(proj1 bs1)) => fs1. move/permutationsP: (s2p) => [bs2 ss2 ts2]; move: (proj1(proj1 bs2)) => fs2. pose s i := Yo (i <c q) (nth_elt K (Vf s1 i)) (Yo (i <c qn) (Vf s2 (i -c q) +c k) (nth_elt K' (i -c qn))). have pa: forall i, i<c q -> s i = (nth_elt K (Vf s1 i)). by move => i liq; rewrite /s; Ytac0. have pb: forall i, i<c q -> inc (s i) K. move => i iq; rewrite (pa _ iq). have p1: inc (Vf s1 i) q by rewrite /q; Wtac; rewrite ss1; apply/(NltP qN). move/(NltP qN): p1 => ha. apply:(nth_elt_inK (NS_lt_nat ha qN) sKN ha). have pc: forall i, qn <=c i -> s i = (nth_elt K' (i -c qn)). rewrite /s => i le1;Ytac h; first by case:(cleNgt qqn (cle_ltT le1 h)). by rewrite (Y_false (cleNgt le1)). have pd: forall i, qn <=c i -> i <c n -> inc (s i) K'. move => i l1 l2; rewrite (pc _ l1); move:(NS_lt_nat l2 nN) => iN. apply:(nth_elt_inK (NS_diff qn iN) sK'N); rewrite cK'. by apply:(cdiff_Mlt kqN iN l1); rewrite csumC qnkq. have pe: forall i, q <=c i -> i <c qn -> s i = (Vf s2 (i -c q) +c k). by move => i l1 l2; rewrite /s (Y_true l2) (Y_false (cleNgt l1)). have pf: forall i, q <=c i -> i <c qn -> [/\ s i = (Vf s2 (i -c q) +c k), inc (Vf s2 (i -c q)) ((n -c k)) & inc (s i) (n -s k)]. move => i l1 l2; rewrite (pe i l1 l2). have iN:= NS_lt_nat l2 qnN. rewrite - {1}(cdiff_pr l1) /qn in l2. have sa:= (csum_lt2l qN (NS_diff q iN) nkN l2). have sb: inc (Vf s2 (i -c q)) (n -c k). by Wtac; rewrite ss2; apply/NltP. move/(NltP nkN):(sb) => sc. move:(csum_Mlteq kN sc); rewrite (csumC (n -c k)) knk => sd. split => //; apply/setC_P; split; first by apply /(NltP nN). move/(NltP kN); move:(Nsum_Mle0 (Vf s2 (i -c q)) kN). move => ua ub; case: (cltNge ub ua). have ax: forall i, inc i n -> inc (s i) n. move => i /(NltP nN) lin. case: (cleT_el (CS_nat qN) (proj31_1 lin)) => le1. case: (cleT_el (CS_nat qnN) (proj31_1 lin)) => le2. by move: (pd i le2 lin) => /setC_P [/sBkBn ha _]. by move:(pf _ le1 le2) =>[_ _ /setC_P []]. by move: (pb i le1) => /Kp /sBkBn. have sjs: forall j, inc j n -> exists2 i, inc i n & j = s i. move => j /(NltP nN) ljn. have jN:= (NS_lt_nat ljn nN). case:(cleT_el (CS_nat kN) (proj31_1 ljn)) => lkj. have l1: (j -c k) <c (n-c k). rewrite - (cdiff_pr lkj) - knk in ljn. exact: (csum_lt2l kN (NS_diff k jN) nkN ljn). move: (perm_int_surj nkN s2p l1) => [i1 l2 iv]. have i1N := NS_lt_nat l2 nkN. have l3:=(csum_Meqlt qN l2). move:(proj31 (pf _ (Nsum_M0le i1 qN) l3)). rewrite {2} csumC (cdiff_pr1 i1N qN) iv (csumC _ k) (cdiff_pr lkj) => <-. exists (q +c i1) => //; apply/(NltP nN); exact:(clt_leT l3 lqnn). case: (inc_or_not j K) => jK. move:(nth_elt_surj sKN qN jK) => [i ia ->]. move:(perm_int_surj qN s1p ia) => [i1 ib <-]. rewrite - (pa _ ib); exists i1 => //; apply/(NltP nN). exact:(clt_ltT ib lqn). have jK': inc j K' by apply/setC_P; split => //; apply/(NltP kN). move:(nth_elt_surj sK'N q'N jK') => [i ia ->]. rewrite cK' in ia. move: (csum_Meqlt qnN ia); rewrite qnkq => /(NltP nN) ic; ex_tac. rewrite (pc _ (Nsum_M0le i qnN)) csumC cdiff_pr1 //. apply:(NS_lt_nat ia kqN). set sigma := Lf s n n. have sp: inc sigma (permutations n). rewrite /sigma; apply/permutationsP; hnf; saw. apply:bijective_if_same_finite_c_surj; aw; trivial. by apply:finite_set_nat. by apply: lf_surjective. ex_tac. move: Xax => [[qa _] qb qd qe]. have: nds_ax (fun z => X (Vf sigma z)) n. rewrite /sigma;move => y /(NltP nN) ys; rewrite LfV//. by move:(ax _ ys) => /(NltP nN) /qa/proj32_1. rewrite /nds_sc - {1 3}qnkq => ax2. have ax3: nds_ax (fun z=> X (Vf sigma z)) (q +c (n -c k)). move => z z1; apply: ax2; rewrite qnkq; exact:(clt_leT z1 lqnn). rewrite (osum_fA qnN kqN ax2) (osum_fA qN nkN ax3) /nds_sc_Ktau/nds_sc. set A := osumf _ _; set B := osumf _ _; set C' := osumf _ _. set A' := osumf _ _; set B' := osumf _ _. have ea: A = A'. apply: (osumf_exten nkN) => i l1. have iB:= NS_lt_nat l1 nkN. move: (csum_Mlteq qN l1) ; rewrite (csumC (n -c k))- /qn => l2. have ha: inc (i +c q) n by apply /(NltP nN); exact:(clt_leT l2 lqnn). move:(Nsum_M0le i qN); rewrite csumC => hb. by rewrite /sigma LfV// (pe _ hb l2) /X2 csumC cdiff_pr1. have eb: B = B'. apply: (osumf_exten qN) => i l1. have ib:inc i n by apply /(NltP nN); exact:(clt_ltT l1 lqn). by rewrite /sigma LfV// - ( pa _ l1). have oa: ordinalp A'. apply:(OS_osumf nkN) => i l1; apply: ax3. by move: (csum_Mlteq qN l1);rewrite (csumC q). have ob: ordinalp B'. apply:(OS_osumf qN) => i l1; apply: ax2; rewrite qnkq. exact:(clt_ltT l1 lqn). have oc: ordinalp C'. apply:(OS_osumf kqN) => i l1; apply: ax2. by rewrite (csumC qn);apply:csum_Mlteq. rewrite (osumA oc oa ob) - ea; apply: (f_equal2 _ _ eb). have knz1:= (cdiff_nz kln). move: (cpred_pr nkN knz1) => [nk1N nk1v]. rewrite /A nk1v (osum_fS _ nk1N) /X2. set C:= osumf _ _ . move: (cltS nk1N); rewrite - nk1v => eq1. have oc': ordinalp C. apply:(OS_osumf nk1N) => i lin. have ha:inc i (source s2). rewrite ss2; apply/(NltP nkN); exact (clt_ltT lin eq1). move:(Vf_target fs2 ha); rewrite ts2 => /(NltP nkN) lt1. by move:(csum_Meqlt kN lt1); rewrite knk => /qa /proj32_1. have ha: inc (cpred (n -c k)) (source s2). by rewrite ss2; apply/(NltP nkN); rewrite {2} nk1v; apply: cltS. move:(Vf_target fs2 ha); rewrite ts2 => /(NltP nkN) lt1. move:(csum_Meqlt kN lt1); rewrite knk => hb. move:(Nsum_M0le (Vf s2 (cpred (n -c k))) kN) => hc. move: (qa _ hb) (qe _ hc hb);set a:= X _ => ap da. rewrite (osumA oc (proj32_1 ap) oc'); congr (_ +o C). rewrite /C'. have hd: forall i, i<c k -c q -> (Vf sigma (i +c qn)) <c k. move => i lik. move:(csum_Meqlt qnN lik); rewrite qnkq => l1. move: (Nsum_M0le i qnN) => l2. move/(NltP nN):(l1) => iN. by rewrite csumC /sigma LfV//; move: (pd _ l2 l1) => /setC_P []/(NltP kN). have he: forall i, i<c k -c q -> let b := X (Vf sigma (i +c qn)) in \0o <o b /\ odegree b = e. move => i l1; move:(hd _ l1) => sa; split. exact: (qa _ (clt_ltT sa kln)). exact:(qd _ sa). symmetry. move:kqN (cleR (CS_nat kqN)). have oa':=(proj32_1 ap). move: {-3} (k -c q); apply: Nat_induction. by rewrite osum_f0 (osum0l oa'). move => i iN Hrec le1. rewrite (osum_fS _ iN). move/(cleSltP iN): (le1) => /he []. set b := (X (Vf sigma (i +c qn))) => bp db. have ikq:=(cleT (cleS iN) le1). have oc'': ordinalp (osumf (fun z : Set => X (Vf sigma (z +c qn))) i). apply: (OS_osumf iN) => j jli. exact: (proj32_1(proj1 (he _ (clt_leT jli ikq)))). rewrite - db in da. rewrite - (osumA (proj32_1 bp) oc'' oa'). by rewrite (Hrec ikq) (ord_negl_p7 bp ap da). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)