proposition: Lemma ord_factor2 p n: ord_factor_list p n -> exists k, ord_factor_boundary p n k.
proof: Proof. move => [nN h1 h2]. set E:= Zo n (fun i => ord_ptypeL (p i)). set F := n -s E. have prop1 i: inc i E -> limit_ordinal (p i). by move => /Zo_hi/ord_ptypeL_prop []. case:(emptyset_dichot F) => Fe. exists n; split => //. - apply: (cleR (CS_nat nN)). - move => i /(NltP nN) => ein; exact:(prop1 _ (empty_setC Fe ein)). - by move => i leni /cltNge. have cF: cardinal_set F by move => i/setC_P [/(NltP nN)/proj31_1 ]. move: (cle_wor' cF Fe); set k := intersection F; move => [kF lkF]. have Ep1 i: natp i -> inc (csucc i) E -> inc i E. move => iN /Zo_P [/(NltP nN) lin tpi ]; apply:Zo_i. by move/(NltP nN):(clt_ltT (cltS iN) lin). move: tpi => [q qa qb]. move:(proj2 (h2 i iN lin) q qa qb) => [b qlb bv]; exists b => //. exact:(proj32 qlb). have Ep2 i: inc i F -> csucc i <c n -> inc (csucc i) F. move => iF sin; apply/setC_P; split;[ by apply/(NltP nN) | move => siE]. move/setC_P: iF => [lin]; case; apply:(Ep1 _ (NS_inc_nat nN lin) siE). have lkn: k <c n by move/Zo_P: kF => [/(NltP nN) ]. exists k; split. - exact: (proj1 lkn). - move => i lik;move/(NltP nN):(clt_ltT lik lkn) => iin. apply: prop1; ex_middle iinE. by move/(setC_P): (conj iin iinE) => /lkF/cleNgt; case. - move => i ha hb. suff h: inc i F. case /ord_prime_p1: (h1 _ hb). + by case/ord_ptypeF_prop. + by case/ord_ptypeI_prop. + by move => hh; case/setC_P:h => ii;case; apply: Zo_i. move:(NS_lt_nat hb nN) => iN. move:i iN ha hb; apply: Nat_induction; first by move => /cle0 => <-. move => i iN Hrec le1 le2; move:(clt_ltT (cltS iN) le2) => le3. case: (cle_eqVlt le1) => lesin; first by rewrite - lesin. move/(cltSleP iN): lesin => lki; exact: (Ep2 _ (Hrec lki le3) le2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)