proposition: Lemma nds_card_different_deg_gen X n: natp n -> opos_below X (csucc n) -> (forall i j, i <c j -> j <=c n -> odegree (X i) <o odegree (X j)) -> nds_ax X (csucc n) /\ nds_card X (csucc n) = \2c ^c n.
proof: Proof. move => nN xp xmon; move: (NS_succ nN) => sN. have ax: nds_ax X (csucc n) by move => i /xp / proj32_1. split => //. move:(NleP nN) (NltP sN) => Ka Kb. rewrite - card_setP; set E := \Po n; set F := (\Po (csucc n)). pose Pe n := (permutations (csucc n)). have Kc s i: inc s (Pe n) -> i <=c n -> Vf s i <c (csucc n). move/permutationsP => [[[fp _] _] ss ts] /Ka ins; apply/Kb; Wtac. have Kc' s i: inc s (Pe n) -> i <=c n -> Vf s i <=c n. by move => h /(Kc _ _ h) /(cltSleP nN). have Kd f i j: inc f (Pe n) -> i <=c n -> j <=c n -> Vf f i = Vf f j -> i = j. move/permutationsP => [[[_ h] _] sf _] /Ka isn /Ka jsn; apply:h; ue. have Hb1 k s: k <=c n -> inc s (Pe n) -> Vf s k = n -> let s2 := nds_sc X k s in ordinalp s2 /\ nds_sc X (csucc n) s = (X n) +o s2. move => lkn sp sk; rewrite /nds_sc. set s2 := osumf (fun z => oopow (Vf s z)) k. have kN:= (NS_le_nat lkn nN). move: (cdiff_pr lkn) (NS_diff k nN); set m := n -c k => mp mN. have eq1 : k +c (csucc (n -c k)) = csucc n by rewrite (csum_nS _ mN) mp. move:(nds_ax_perm sN ax sp); rewrite - eq1; move=> [sax oo1]. rewrite(osum_fA kN (NS_succ mN) sax) -/s2. split; last (apply: f_equal2; last exact). apply: (OS_osumf kN) => i li; apply: ax; apply/ (Kc _ _ sp). by apply: (cleT (proj1 li) lkn). have qa: opos_below (fun z => X (Vf s (z +c k))) (csucc m). move => i il1; apply: xp;apply: (Kc _ _ sp). by rewrite - mp csumC; apply: csum_Meqle; apply/cltSleP. rewrite (osum_negl_recd mN qa) ? (Nsum0l kN) ? sk //. move => i lim; apply: (xmon _ _ _ (cleR (CS_nat nN))). have iN := (NS_lt_nat lim mN). have pa: (csucc i +c k) <=c n. by rewrite - mp csumC; apply(csum_Meqle); apply/(cleSltP iN). move: (Kc' _ _ sp pa) => /cle_eqVlt; rewrite - sk;case => //. move / (Kd s _ k sp pa lkn). rewrite -{2} (Nsum0l kN). by move/(csum_eq2r kN (NS_succ iN) NS0) =>h; case:(@succ_nz i). pose ii f := Vf (inverse_fun f) n. pose pa f k := forall i j, i<c j -> j <c k -> f i <c f j. pose mxi f := \csup (Zo (csucc (csucc n)) (pa (Vf f))). have mxia f: let k := (mxi f) in inc f (Pe n) -> [/\ natp k, \0c <c k, k <=c csucc n, pa (Vf f) k & k = (csucc n) \/ Vf f k <c Vf f (cpred k)]. move => k fp. set T := (Zo (csucc (csucc n)) (pa (Vf f))). have qa i: inc i T -> i <=c csucc n by move => /Zo_S /(NleP sN). move:(Nat_sup_pr sN qa); rewrite /T -/(mxi _) -/k => - [ra rb rc rd]. have zT: inc \1c T. apply/Zo_P; split. by rewrite - succ_zero; apply/(NleP sN); apply:cleSS; apply:cle0n. by move => i j lij /clt1 ej0; move: lij; rewrite ej0 => /clt0. move: (rc _ zT) => /cge1P kp. have re: inc k T by case: rd => // /set0_P => h;case: (h \1c). move/Zo_P: re => [_ re]. split => //. case /cle_eqVlt: rb; [ by left | move => ll; right]. case: (p_or_not_p (pa (Vf f) (csucc k))) => hpa. have: (inc (csucc k)) T. by apply: Zo_i => //; apply/ (NleP sN); apply/cleSltP. by move/rc /cltNge; case; apply: cltS. ex_middle h. case: hpa => i j lij /(cltSleP ra) /cle_eqVlt; case; last by apply: re. move => jv. case: (equal_or_not k \0c) => knz; first by move:lij;rewrite jv knz => /clt0. move: (cpred_pr ra knz) =>[pN pv]. have tN x: x <=c n -> natp (Vf f x). move/(Kc' _ _ fp) => hw; apply/(NS_le_nat hw nN). have l3: cpred k <c k by rewrite {2} pv; apply: cltS. move/(cltSleP nN): ll => ksf; move: (cleT (proj1 l3) ksf) => pksf. case: (NleT_ell (tN _ ksf) (tN _ pksf)). by move/(Kd _ _ _ fp ksf pksf) => h'; case:(proj2 (cltS pN)); ue. done. move: lij; rewrite jv {1} pv => /(cltSleP pN); case /cle_eqVlt. by move ->. move => lipk l4; exact: (clt_ltT (re i (cpred k) lipk l3) l4). have mxib f k i: inc f (Pe n) -> pa (Vf f) k -> k <=c csucc n -> i <c k -> i <=c Vf f i. move => fp pak lkn lik. move: (NS_lt_nat (clt_leT lik lkn) sN) => iN. move/permutationsP: fp => [[[ff injf] sjf] sf tf]. move: i iN lik; apply: Nat_induction. move => w; move /(NltP sN): (clt_leT w lkn). rewrite - sf =>/(Vf_target ff); rewrite tf => /(NleP nN). by move/proj31 => cc; apply:(cle0x cc). move => i iN Hrec lei; move: (cltS iN) => liN. apply/(cleSltP iN); apply: (cle_ltT (Hrec (clt_ltT liN lei))). exact: (pak i (csucc i) liN lei). have mxic f: inc f (Pe n) -> mxi f = csucc n -> Vf f n = n. move => fp; move: (mxia f fp) => [kN kp ksn pak _] eksn. apply: cleA;first by apply/(Kc' _ _ fp (cleR (CS_nat nN))). by apply: (mxib _ _ _ fp pak ksn); rewrite eksn; apply: cltS. have iip f: inc f (Pe n) -> [/\ Vf f (ii f) = n, ii f <=c n & forall x, x <=c n -> Vf f x = n -> x = ii f]. move/permutationsP =>[ bf sf tf]; move: (Nsucc_i nN) => h. have fk1: Vf f (ii f) = n. by rewrite /ii (inverse_V bf) //; rewrite tf. have lt2: (ii f) <=c n. apply/Ka; rewrite - sf. by apply: (inverse_Vis bf); rewrite tf. rewrite -{4} fk1; split=> // x fx. by apply/(proj2 (proj1 bf)); rewrite sf; apply/Ka. have mxid f: inc f (Pe n) -> Vf f (cpred (mxi f)) <c n -> exists f', [/\ inc f' (Pe n), ii f' <c ii f & nds_sc X (csucc n) f = nds_sc X (csucc n) f' ]. move => fp le1. move: (mxia f fp); set k := mxi f; move => [kN kp ksn pak aux]. have nkn: k = csucc n -> False. move => h;case: (proj2 le1); rewrite -/k h (cpred_pr1 (CS_nat nN)). by apply: mxic. case: aux => lt1; first by case: nkn. case: (cle_eqVlt ksn);[ by move => h;case nkn| move/(cltSleP nN) => lekn]. case: (iip _ fp); set k1 := ii f => fk1 lt2 etc. move/permutationsP: (fp) => [bf sf tf]. have ff := (proj1 (proj1 bf)). move: (cpred_pr kN (nesym (proj2 kp))) =>[pN pv]. have lt3: cpred k <=c n. by apply/(cleSSP (CS_nat pN) (CS_nat nN)); rewrite - pv. case: (cleT_ell (proj31 lt2) (proj31 ksn)) => lt4. by move:lt1; rewrite - {1} lt4 fk1 => /cltNge; case; apply: Kc'. move: lt4; rewrite pv => /(cltSleP pN); case/cle_eqVlt => lt5. by case: (proj2 le1); rewrite -/k; rewrite - lt5. move: (cltSS lt5); rewrite - pv => lt6. move: (pak k1 (csucc k1) (cltS (NS_le_nat lt2 nN)) lt6); rewrite fk1. case /cltNge; apply: (Kc' _ _ fp (cleT (proj1 lt6) lekn)). pose f1 i := Yo (i <c k) (Vf f i) (Yo (i <c k1) (Vf f (csucc i)) (Yo (i = k1) (Vf f k) (Vf f i))). have ax1: lf_axiom f1 (csucc n) (csucc n). have ksf: inc k (source f) by rewrite sf; apply/NleP. move => i lin; rewrite /f1; Ytac qa; [ Wtac | Ytac qb; last Ytac qc; Wtac]. move: (clt_leT qb lt2) => likn. by rewrite sf; apply/(NleP nN); apply/(cleSltP (NS_lt_nat likn nN)). pose f2 := Lf f1 (csucc n) (csucc n). have sjf2: surjection f2. apply: (lf_surjective ax1) ; rewrite -{1} tf => y /(proj2(proj2 bf)). move => [i isf ->]; rewrite sf in isf. have iN := (NS_inc_nat sN isf). rewrite /f1. case: (NleT_el kN iN) => lt5; last by exists i => //; Ytac0. move: (cleNgt lt5) => lt54. case: (cle_eqVlt lt5) => lt6. exists k1; first by apply/Ka. Ytac0; rewrite (Y_false(cleNgt (proj1 lt4))) - lt6 Y_false => //. by case. have k1N := NS_le_nat lt2 nN. case: (NleT_el iN k1N) => lt7; last first. by move: lt7=> [/cleNgt qa qb]; exists i => //;Ytac0; Ytac0; Ytac0. have inz: i <> \0c by move => iz;move: lt6; rewrite iz => /clt0. move: (cpred_pr iN inz) =>[jN jv]. have lt8: cpred i <c i by rewrite {2} jv; apply: cltS. exists (cpred i); first by apply/Ka; apply: (cleT (proj1 lt8)); apply/Ka. rewrite (Y_true (clt_leT lt8 lt7)) -jv Y_false //; apply: cleNgt. by apply /(cltSleP jN); rewrite - jv. have bf2: bijection f2. rewrite /f2; apply:bijective_if_same_finite_c_surj; aw; trivial. apply: (finite_set_nat sN). have f2p: inc f2 (Pe n). by rewrite/f2;apply/permutationsP; saw. move: (cpred_pr (NS_le_nat lt2 nN) (card_gt_ne0 lt4)) => [k2N k2v]. move: (cltS k2N); rewrite - k2v => lt9. move: (cleT (proj1 lt9) lt2) => le10. have qa: inc (cpred k1) (csucc n) by apply/Ka. move: lt4; rewrite {1} k2v => /(cltSleP k2N) => lt10. have f2sk: Vf f2 (cpred k1) = n. move /cleNgt: lt10 => lt10. by rewrite /f2 LfV//; rewrite /f1; Ytac0; Ytac0; rewrite - k2v. have iif2 : ii f2 <c k1. have qb: inc (cpred k1) (source f2) by rewrite /f2; aw. by move: (inverse_V2 bf2 qb); rewrite /ii f2sk => ->. exists f2; split => //. move: (cdiff_pr lt10) (NS_diff k k2N); set k2 := _ -c _ => eqa d1N. move: (Hb1 _ _ lt2 fp fk1) => [os1 ->]. move: (Hb1 _ _ le10 f2p f2sk) => [os2 ->]; apply: f_equal. rewrite /nds_sc. set Y1 := (fun z : Set => X (Vf f z)). set Y2 := (fun z : Set => X (Vf f2 z)). have Ke i: i <=c n -> ordinalp (Y1 i). by move => iln; move: (proj32_1 (xp _ (Kc _ _ fp iln))). have ax3: nds_ax Y1 k1. move => i lik; apply: (Ke _ (cleT (proj1 lik) lt2)). have ax4: nds_ax (fun z => Y1 (z +c k)) (csucc k2). move => i /(cltSleP d1N) lik; apply:Ke. move:(csum_Meqle k lik); rewrite csumC eqa => qc; apply: (cleT qc le10). have ax2: nds_ax Y2 (cpred k1). move => i lin. move: (cleT (proj1 lin) le10) => /Ka lt12. by rewrite /Y2/f2 LfV//;move/(NltP sN):(ax1 _ lt12) => /xp/proj32_1. rewrite - eqa in ax2. rewrite - eqa (osum_fA kN d1N ax2). have eqc : k +c (csucc k2) = k1 by rewrite k2v - eqa csum_nS. rewrite - eqc in ax3. rewrite - eqc (osum_fA kN (NS_succ d1N) ax3). rewrite (osum_f1r d1N ax4) (csum0l (CS_nat kN)). set U := osumf (fun i => Y1 (csucc i +c k)) k2. have ->: osumf (fun z => Y2 (z +c k)) k2 = U. apply: (osumf_exten d1N) => i lik; rewrite /Y1 /Y2 /f2/f1. have lt11: i +c k <c k1. apply: clt_ltT lt9; rewrite - eqa csumC; apply: (csum_Meqlt kN lik). move/Ka: (cleT (proj1 lt11) lt2) => lt13. move:(cleNgt (csum_Mle0 i (CS_nat kN))) => lt12. by rewrite LfV//; Ytac0; Ytac0; rewrite (csum_Sn _ (NS_lt_nat lik d1N)). have y1kp: \0o <o Y1 k by apply: xp; apply/(Kc _ _ fp). have y1pkp: \0o <o Y1 (cpred k) by apply: xp; apply/(Kc _ _ fp). have oU: ordinalp U. apply: OS_osumf => // i lin; apply: ax3; rewrite csumC. by apply: (csum_Meqlt kN); apply: cltSS. have oy1 := (proj32_1 y1kp). have oy3 := (proj32_1 y1pkp). have oy2: ordinalp (osumf Y1 k). by apply: (OS_osumf kN) => i lin; apply: (Ke _ (cleT (proj1 lin) lekn)). have oy4: ordinalp (osumf Y1 (cpred k)). apply: (OS_osumf pN) => i lin; exact: (Ke _ (cleT (proj1 lin) lt3)). rewrite - (osumA oU oy1 oy2); apply: f_equal. have ->: osumf Y2 k = osumf Y1 k. apply: (osumf_exten kN) => i lik; rewrite /Y1 /Y2 /f2/f1. rewrite LfV//; [ by Ytac0 | apply/Ka; apply: (cleT (proj1 lik) lekn)]. rewrite {2 3} pv (osum_fS _ pN). rewrite (osumA oy1 oy3 oy4). have lt12: Vf f (cpred k) <=c n by apply/Kc'. by rewrite (ord_negl_p7 y1kp y1pkp (xmon _ _ lt1 lt12)). have mixe f: inc f (Pe n) -> exists f', [/\ inc f' (Pe n), pa (Vf f') (ii f') & nds_sc X (csucc n) f = nds_sc X (csucc n) f' ]. move => hyp. set T := Zo (Pe n) (fun s => nds_sc X (csucc n) f = nds_sc X (csucc n) s). suff: exists2 f', inc f' T & pa (Vf f') (ii f'). by move => [s /Zo_P [qa qb] qc]; exists s. have hu s: inc s T -> Vf s (cpred (mxi s)) <c n -> exists2 s', inc s' T & ii s' <c ii s. move => /Zo_P [sa sb] sc; move: (mxid _ sa sc) => [s' [sd se sf]]. by rewrite /T;exists s' => //; rewrite sb sf; apply Zo_i. set W := fun_image T ii. have neW: nonempty W by apply: funI_setne; exists f; apply/Zo_i. have sWn: sub W Nat. by move => y /funI_P [s /Zo_P [/iip [_ qa _] _] ->];apply: (NS_le_nat qa nN). move: (inf_Nat sWn neW); set im := intersection _; move => [mW iml]. move: mW =>/funI_P[s sT sm]. move/Zo_P: (sT) => [qa qb]. move: (mxia _ qa) =>[ra rb rc rd re]. move: (cpred_pr ra (nesym(proj2 rb))) => [sa sb]. move: (rc);rewrite {1} sb =>/(cleSltP sa) /(cltSleP nN) /(Kc' _ _ qa). case/cle_eqVlt; last first. move=> /(hu _ sT) [s' qc]; rewrite - sm => /cltNge; case. apply: iml. apply/funI_P; ex_tac. move => eqa; exists s => //. have ->: ii s = (cpred (mxi s)). move/permutationsP: qa => [bf sf tf]. rewrite /ii - eqa (inverse_V2 bf) //; rewrite sf; apply/Ka. apply/(cleSSP (CS_nat sa) (CS_nat nN)). ue. move => i j lij ljk; apply: (rd i j lij); rewrite sb. exact: (clt_ltT ljk (cltS sa)). set G := (nds_sums X (csucc n)). pose pe x f := [/\ inc f (Pe n), pa (Vf f) (ii f) & nds_sc X (csucc n) f = x]. pose fu x := choose (pe x). have fup x: inc x G -> pe x (fu x). move => xe; apply:choose_pr. by move:xe => /funI_P [f /mixe [f' [qa qb ->]] ->]; exists f'. pose fv s := fun_image (ii s) (Vf s). have fvp f: inc f (Pe n) -> pa (Vf f) (ii f) -> cardinal (fv f) = ii f. move => fp pak; move: (iip _ fp) => [qa qb _]. rewrite /fv - {2} (card_card (proj31 qb)); apply:cardinal_fun_image. move:(NS_le_nat qb nN) => kN. move => i j /(NltP kN) l1 /(NltP kN) l2 ee. case: (cleT_ell (proj31_1 l1) (proj31_1 l2)) => lij; first by rewrite lij. by move: (proj2 (pak i j lij l2)). by case: (proj2 (pak j i lij l1)). have axg f: inc f (Pe n) -> pa (Vf f) (ii f) -> inc (fv f) E. move => qa qb; apply/setP_P => u/funI_P [j ja ->]. move: (iip _ qa) => [qd qe qf]. move/(NltP (NS_le_nat qe nN)): ja => ja; move:(cleT (proj1 ja) qe) => l1. apply/(NltP nN); split; first by apply/(Kc' _ _ qa). move => ee; case: (proj2 ja); exact: (qf _ l1 ee). have axf x: inc x G -> inc (fv (fu x)) E. by move/fup=> [qa qb qc]; apply: axg. have Hb2 f: inc f (Pe n) -> let s2 := nds_sc X (ii f) f in ordinalp s2 /\ nds_sc X (csucc n) f = X n +o s2. move => h; move: (iip _ h) => [qa qb qc]. exact: (Hb1 _ _ qb h qa). have rinj u v : inc u G -> inc v G -> fv (fu u) = fv (fu v) -> u = v. move => /fup [qa qb qc] /fup [qa' qb' qc'] sfi. rewrite -qc - qc'. rewrite (proj2 (Hb2 _ qa)) (proj2 (Hb2 _ qa')); apply: f_equal. move: (iip _ qa) (iip _ qa')=> [i1 i2 i3] [i1' i2' i3']. have: ii (fu u) = ii (fu v). by rewrite - (fvp _ qa qb) - (fvp _ qa' qb') -/(fv _) sfi. set k := ii (fu u) => kv. have kN:= (NS_le_nat i2 nN). rewrite - kv; apply: (osumf_exten kN) => i lik; congr X; move: i lik. suff: forall m, natp m -> forall i, i <c m -> i <c k -> Vf (fu u) i = Vf (fu v) i. by move => H i lik; apply: (H k kN i lik lik). apply: Nat_induction; first by move => i /clt0. move => m mN Hrec i /(cltSleP mN); case/(cle_eqVlt); last by apply: Hrec. move => -> lik. have: inc (Vf (fu u) m) (fv (fu u)) by apply: funI_i; apply /(NltP kN). rewrite sfi /fv - kv => /funI_P [j /(NltP kN)ljk eqa]. move/permutationsP: qa => [[[_ ra] rb] sf tf]. have aux t: t <c k -> inc t (source (fu u)). rewrite sf => tk; apply/(NleP nN); exact: (cleT (proj1 tk) i2). case: (cleT_ell (proj31_1 ljk) (CS_nat mN)) => lmj. by rewrite eqa lmj. move: (Hrec j lmj ljk); rewrite - eqa => ss; case: (proj2 lmj). by apply: ra => //; apply: aux. rewrite -/k kv in ljk; move: (qb' _ _ lmj ljk); rewrite - eqa => /proj1 lt1. clear ra rb sf tf j lmj ljk eqa aux. have:inc (Vf (fu v) m) (fv (fu v)). by apply: funI_i; rewrite -kv;apply /(NltP kN). rewrite - sfi /fv => /funI_P [j /(NltP kN)ljk eqa]. move/permutationsP: qa' => [[[_ ra] rb] sf tf]. have aux t: t <c k -> inc t (source (fu v)). rewrite sf => tk; apply/(NleP nN); exact: (cleT (proj1 tk) i2). case: (cleT_ell (proj31_1 ljk) (CS_nat mN)) => lmj. by rewrite eqa lmj. move: (Hrec j lmj ljk); rewrite - eqa => ss; case: (proj2 lmj). by apply: ra => //; apply: aux. by move: (qb _ _ lmj ljk); rewrite - eqa => /cltNge; case. suff Hc s1 s2: inc s1 (Pe n) -> inc s2 (Pe n) -> pa (Vf s1) (ii s1) -> pa (Vf s2) (ii s2) -> nds_sc X (csucc n) s1 = nds_sc X (csucc n) s2 -> fv s1 = fv s2. suff: bijection (Lf (fun t => (fv (fu t))) G E). by rewrite /nds_card; move/card_bijection; aw. apply: lf_bijective => //. move => y yE; move:(nth_elt_dbl_prop1 nN yE). set f := Lf _ _ _; move => [fp ys yv fk pak]. set t := (nds_sc X (csucc n) f). have tG: inc t G by apply/funI_P; ex_tac. ex_tac; rewrite /fv yv. move:(fup _ tG)=> [qa qb qc]. have ra: cardinal y = ii f. move/permutationsP: fp => [bf sf tf]. by rewrite /ii - fk (inverse_V2 bf) // sf; apply/Ka. rewrite ra in pak *. by apply: (Hc _ _ fp qa pak qb); rewrite qc. clear mxi mxia mxib mxic mxid rinj. move => fp1 fp2 pa1 pa2. move: (Hb2 _ fp1) (Hb2 _ fp2) => [os1 ->] [os2 ->]. move /(osum2_simpl os1 os2 (ax _ (cltS nN))); rewrite /nds_sc. pose Ht m := opos_below X m /\ (forall i j, i <c j -> j <c m -> odegree (X i) <o odegree (X j)). have: Ht n. split; first by move => i lin; apply: xp; apply: (clt_ltT lin (cltS nN)). by move => i j lij /proj1 ljn; apply: xmon. set K1 := fv s1; set K2 := fv s2. pose q n K f := [/\ sub K n, K = fun_image (cardinal K)f & pa f (cardinal K)]. move: (fvp _ fp2 pa2); rewrite -/K2 => aux1. move: (fvp _ fp1 pa1); rewrite -/K1 => aux2. have: q n K2 (Vf s2). hnf; rewrite aux1; split => //; by apply/setP_P; apply: axg. have: q n K1 (Vf s1). hnf; rewrite aux2; split => //; by apply/setP_P; apply: axg. rewrite - aux1 - aux2; clear aux1 aux2. set f1 := Vf s1; set f2 := Vf s2; move: K1 K2 f1 f2. clear Hb1 G axf fu fup fv fvp axg. clear ii iip mixe pe Hb2 pa1 pa2 os1 os2. clear sN E F ax s1 s2 xp xmon fp1 fp2 Ka Kb Kc Kc' Kd. move: n nN. have prop0 n K: natp n -> sub K (csucc n) -> ~inc n K -> sub K n. move => nN ha h t tK. move: (ha _ tK)=> /(NltP (NS_succ nN)) /(cltSleP nN) /cle_eqVlt; case. by move => tn; case: h; rewrite - tn. by move/(NltP nN). have prop1 n K : natp n -> sub K n -> natp (cardinal K). by move => nN /sub_smaller; rewrite (card_nat nN) => x; apply (NS_le_nat x). have hw n K f: natp n -> sub K n -> (forall i, i <c cardinal K -> inc (f i) K) -> Ht (csucc n) -> osumf (fun z => X (f z)) (cardinal K) <o X n. move => nN ha hb [ht1 ht2]. apply: (olt_leT _ (proj1 (the_cnf_p4 (ht1 _ (cltS nN))))). have ii:=(indecomp_prop4 (OS_degree (proj32_1 (ht1 _ (cltS nN))))). have: forall i, i <c (cardinal K) -> X (f i) <o oopow (odegree (X n)). move => i /hb /ha /(NltP nN) => fin. apply:(olt_leT (proj2 (the_cnf_p4 (ht1 _ (clt_ltT fin (cltS nN)))))). apply:opow_Mo_le; apply/oleSltP;exact: (ht2 _ _ fin (cltS nN)). move: (prop1 _ _ nN ha). move:(cardinal K); apply:Nat_induction. move => _; rewrite osum_f0; exact: (proj1 ii). move => m mN Hr ax; move: (true_below_rec mN ax) => [ax1 ax2]. rewrite (osum_fS _ mN). apply:(indecomp_prop2 ax2 (Hr ax1) ii). have prop3 n K f: let K1 := K -s1 n in let k1 := cpred (cardinal K) in natp n -> q (csucc n) K f -> inc n K -> [/\ [/\ cardinal K = csucc (cardinal K1), natp (cardinal K1) & k1 = cardinal K1], k1 <c cardinal K, f k1 = n , forall i, i <c cardinal K1 -> inc (f i) K1 & q n (K -s1 n) f]. move => /= nN [qa qb qd] nK; move: (NS_succ nN) => snN. move: (cpred_pr5 nK) (csucc_pr2 nK). have Kn:= (prop1 _ _ snN qa). set k := cpred _; set k' := cardinal _ => eq1 eq2. have ckz: cardinal K <> \0c by rewrite eq2; apply: succ_nz. move: (cpred_pr Kn ckz); rewrite - eq1 -/k; move => [kN eq3]. move: (cltS kN); rewrite - eq3 eq1 =>lt1. move: nK; rewrite {1} qb => /funI_P [i /(NltP Kn) lik fv]. move: lik; rewrite {1} eq3 =>/(cltSleP kN); move/(NltP Kn):(lt1) => lt2. rewrite {1} eq1 ;move/cle_eqVlt; case => ik1; last first. case: (cltNge (qd _ _ ik1 lt1)); rewrite - fv. by apply /(cltSleP nN)/(NltP snN) /qa; rewrite qb; apply: funI_i. rewrite ik1 in fv; clear i ik1. move: (kN); rewrite eq1 => kN'. have hu: forall i, i <c k' -> inc (f i) (K -s1 n). move => i lik; apply/setC1_P. move/(NltP Kn) : (clt_ltT lik lt1) => ik2. have fik:inc (f i) K by rewrite qb; apply funI_i. by split => // eq4; case: (proj2 (qd _ _ lik lt1)); rewrite eq4 fv. split => //; split. - by apply:(prop0 _ _ nN); [ move => t/setC1_P [/qa] | move=> /setC1_P [_]]. - rewrite {1} qb; set_extens t. move => /setC1_P [/funI_P [i lik ->] fjn]; apply/funI_P; exists i => //. apply/(NltP kN'); split; last by move => ba; case: fjn; ue. by apply/(cltSleP kN'); rewrite - eq2; apply /NltP. move/funI_P =>[i /(NltP kN') lik ->]; rewrite - qb; apply/setC1_P. move/(NltP Kn) : (clt_ltT lik lt1) => ik2. have fik:inc (f i) K by rewrite qb; apply funI_i. by split => // eq4; case: (proj2 (qd _ _ lik lt1)); rewrite eq4 fv. - move => i j lij ljk; apply:(qd _ _ lij (clt_ltT ljk lt1)). apply: Nat_induction. by move => K K' f f'' [ /sub_set0 -> _ _] [/sub_set0 -> _ _] _. move => n nN Hrec K K' f f' qp qp' Htt. have sN := NS_succ nN. have pa' t: inc t (csucc n) -> inc t n \/ t = n. move/(NltP sN) /(cltSleP nN) /cle_eqVlt; case; first by right. by move/(NltP nN); left. move: (qp) (qp')=> [pr1 pr2 pr4] [pr1' pr2' pr4']. move: (prop0 _ _ nN pr1) (prop0 _ _ nN pr1') => hu hv. have cKN:= prop1 _ _ sN pr1; have cKN':= prop1 _ _ sN pr1'. have ax0 i: inc i (csucc n) -> ordinalp (X i). move/(NltP sN) => lin; exact: (proj32_1 ((proj1 Htt) _ lin)). have hx: nds_ax (fun z => X (f z)) (cardinal K). by move => i /(NltP cKN) ii;apply:ax0; apply: pr1; rewrite pr2;apply: funI_i. have hx': nds_ax (fun z => X (f' z)) (cardinal K'). move => i /(NltP cKN') ii;apply:ax0. by apply: pr1'; rewrite pr2';apply: funI_i. have Htn : Ht n. split; first by exact: (proj1 (true_below_rec nN (proj1 Htt))). by move => i j lij ljn; apply: (proj2 Htt i j lij (clt_ltT ljn (cltS nN))). case: (inc_or_not n K) => inK; case: (inc_or_not n K') => inK'. - move: (prop3 _ _ _ nN qp inK). set K1 := K -s1 n; set k1 := cpred _. move => [[k1v k1N k2v] lt1 fk1 fk2 qp1]. move: (prop3 _ _ _ nN qp' inK'). set K1' := K' -s1 n; set k1' := cpred _. move => [[k1v' k1N' k2v'] lt1' fk1' fk2' qp1']. have ax1: ordinalp (osumf (fun z => X (f z)) k1). apply: (OS_osumf (NS_lt_nat lt1 cKN)) => i ii. apply: (hx _ (clt_ltT ii lt1)). have ax1': ordinalp (osumf (fun z => X (f' z)) k1'). apply: (OS_osumf (NS_lt_nat lt1' cKN')) => i ii. apply: (hx' _ (clt_ltT ii lt1')). have o3:= (proj32_1 (proj1 Htt _ (cltS nN))). rewrite k1v k1v' (osum_fS _ k1N) (osum_fS _ k1N') - k2v fk1 - k2v' fk1'. move/(osum2_simpl ax1 ax1' o3); rewrite k2v k2v' => ss. rewrite - (setC1_K inK) - (setC1_K inK'). by rewrite -/K1 (Hrec _ _ _ _ qp1 qp1' Htn ss). - move: (hv inK') => ra eq0. have r4: forall i, i <c cardinal K'-> inc (f' i) K'. by rewrite {2} pr2' => i lik; apply: funI_i; apply/NltP. move: (hw _ _ _ nN ra r4 Htt); rewrite - eq0 => lt1. move: (prop3 _ _ _ nN qp inK) => [_ qb qc qd]. by case: (oleNgt (osum_Mon1 cKN qb hx)); rewrite qc. - move: (hu inK) => ra eq0 . have r4: forall i, i <c cardinal K-> inc (f i) K. by rewrite {2} pr2 => i lik; apply: funI_i; apply/NltP. move: (hw _ _ _ nN ra r4 Htt); rewrite eq0 => lt1. move: (prop3 _ _ _ nN qp' inK') => [qa qb qc qd]. by case: (oleNgt (osum_Mon1 cKN' qb hx')); rewrite qc. - by move: (hu inK) (hv inK') => ra rb; apply: Hrec. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)