proposition: Lemma nds_tn_prop2 n X: natp n -> \0c <c n -> nds_tn_ax X n -> (nds_tn_S X n) = unionf n (fun a => fun_image (\Po (n -s1 a)) (fun K => oopow (odegree (X \0c)) *o (csumb (K +s1 a) (the_cnf_lc \o X)) +o the_cnf_rem (X a))) +s1 \0c.
proof: Proof. move => nN np ax. set ee := (odegree (X \0c)). have nds_tn_axE i: i <c n -> [/\ \0o <o (the_cnf_lc (X i)), (the_cnf_lc (X i)) <o omega0, the_cnf_rem (X i) <o oopow ee & X i = oopow ee *o (the_cnf_lc (X i)) +o (the_cnf_rem (X i))]. move => lin. move: ax => [ax1 [e ea eb]]. by move: (the_cnf_split (ax1 i lin)); rewrite (eb _ lin) /ee (eb _ np). have tn8 K s: inc K (\Po n) -> inc s (permutations (cardinal K)) -> nonempty K -> nds_sc_Ktau X K s = oopow ee *o nds_sc_K (the_cnf_lc \o X) K +o the_cnf_rem (X (nth_elt K (Vf s \0c))). set m := cardinal K;move => /setP_P sb sp nek. move:(sub_smaller sb); rewrite (card_nat nN); rewrite -/m => ckn. have mN:=(NS_le_nat ckn nN). have mz:= (card_ne0_pos (CS_nat mN) (card_nonempty1 nek)). pose c z := the_cnf_lc (X (nth_elt K z)). pose r z := the_cnf_rem (X (nth_elt K z)). have aux: forall i, i <c m -> [/\ \0o <o c i, c i <o omega0, r i <o oopow ee & X (nth_elt K i) = oopow ee *o c i +o r i ]. move => i l1. have sKN: sub K Nat by move => t /sb/(NltP nN) => h; apply(NS_lt_nat h nN). move: (nth_elt_inK (NS_lt_nat l1 mN) sKN l1) => /sb/(NltP nN). by move/nds_tn_axE. have h2: ordinalp ee. by move:(proj2 ax) => [e ea eb]; rewrite /ee (eb _ np). have h3 i: i <c m-> \0o <o c i /\ r i <o omega0 ^o ee by move => /aux []. have h4 i: i <c m -> c i <o omega0 by move => /aux[]. have -> : nds_sc_K (the_cnf_lc \o X) K = osumf c m. by rewrite osum_of_nat // => i /h4 /olt_omegaP. rewrite /nds_sc_Ktau -(nds_same_deg_s_perm mN mz h2 h3 h4 sp). apply:(osumf_exten mN) => i /(NltP mN) lin. have /aux [_ _ _]//: (Vf s i) <c m. apply/(NltP mN). move/(permutationsP): sp => [[[fs _] _] ss ts]; Wtac. have H s: nds_sc_Ktau X emptyset s = \0c. by rewrite /nds_sc_Ktau cardinal_set0/nds_sc osum_f0. set c := (the_cnf_lc \o X). set_extens v. move/setUf_P => [K ka /funI_P [s sp sv]]. case:(emptyset_dichot K) => ke; first by rewrite sv ke H; fprops. apply/setU1_P; left; apply /setUf_P. move: (nth_elt_prop7 nN ka sp ke); set a := (nth_elt K (Vf s \0c)) => ak. move/setP_P:(ka) => kb. have an: inc a n by apply: kb. ex_tac; apply /funI_P;exists (K -s1 a). by apply/setP_P => t/setC1_P [ha hb]; apply/setC1_P; split=> //; apply: kb. by rewrite sv (tn8 _ _ ka sp ke) (setC1_K ak) (nds_sc_Kval c nN ka). case/setU1_P => h1; last first. rewrite h1; apply/setUf_P; exists emptyset; first by apply: setP_0i. apply/funI_P; exists (identity (cardinal emptyset)); last by rewrite H. apply:permutation_id. move/setUf_P: h1 => [a aN /funI_P[K /setP_P Kb ->]]. have nk1: ~ (inc a K) by move /Kb => /setC1_P[]. have eq1:= setU1_K nk1. have ha: inc (K +s1 a) (\Po n). apply /setP_P => t/setU1_P; case; [by move/Kb => /setC1_P[] | by move ->]. have hb: inc a (K +s1 a) by fprops. have Kne: nonempty (K +s1 a) by ex_tac. move: (nth_elt_prop8 nN ha hb) => [f fp aaa]. apply/setUf_P; ex_tac;apply/funI_P; ex_tac. by rewrite (tn8 _ _ ha fp Kne) - aaa (nds_sc_Kval c nN ha). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)