proposition: Lemma CNFB_e_p9 x: ordinalp x -> exists2 n, natp n & CNFB_expos_rec_nc x n = emptyset.
proof: Proof. move=> ox; ex_middle aux. have pa: forall n, natp n -> nonempty (CNFB_expos_rec_nc x n). move=> n nB; case: (emptyset_dichot (CNFB_expos_rec_nc x n)) => //. by move => p; case: aux; exists n. pose T := (CNFB_expos_rec_nc x). pose h n := \osup (T n). have hp: forall n, natp n -> [/\ (forall a, inc a (T n) -> a <=o h n), inc (h n) (T n) & forall a, inc a (T (csucc n)) -> a <o (h n)]. move=> n nB; move: (CNFB_e_p7 ox nB) => [fs os]. have sT: sub (T n) (Vf(CNFB_expos_rec x) n) by apply: Zo_S. have osT: ordinal_set (T n) by move=> t aT; apply (os _ (sT _ aT)). have pX: (forall a : Set, inc a (T n) -> a <=o h n). by move=> a aT; apply: ord_sup_ub. have pY: inc (h n) (T n). move:(wordering_ole_pr osT). set r := (ole_on (T n)); move=> [wor sr]. move: (worder_total wor) => tor. have srt: sub (T n) (substrate r) by rewrite sr; fprops. move: (sub_finite_set sT fs) => fsT. move: (finite_subset_torder_greatest tor fsT (pa _ nB) srt) => [g gr]. move: tor => [or _]. move: gr => []; rewrite iorder_sr // => p1 p2. have <- //: g = h n. apply: (oleA); first by apply: ord_sup_ub. apply: ord_ub_sup => //; first by apply: osT. move=> i iT; move: (iorder_gle1 (p2 _ iT)). by move /graph_on_P1 => [_ _]. split => //. move => a /Zo_P [qa qb]. move: (induction_defined_pr (fun z => union (fun_image z CNFB_expos)) (CNFB_expos x)); rewrite -/ (CNFB_expos_rec x). move=> [_ _ _ gnz]. move: qa; rewrite (gnz _ nB) => /setU_P [y ay] /funI_P [z zT yv]. rewrite yv in ay. move: (CNFB_e_p6 (os _ zT)) => [zp zq]. case: (p_or_not_p (b_critical z)) => zc. by case: qb; move: ay; rewrite (zp zc) => /set1_P ->. move: ((zq zc) _ ay) => z1. by apply: (olt_leT z1); apply:pX; apply: Zo_i. have xx: forall n, natp n -> h (csucc n) <o h n. move=> n nB; move: (hp _ nB) => [_ _ p3]; apply: p3. by move:(hp _ (NS_succ nB)) => [_ p2 _]. set R:= fun_image Nat h. have neR: nonempty R by exists(h \0c); apply /funI_P; exists \0c => //; apply:NS0. have osR: ordinal_set R. by move =>t /funI_P [n nB ->]; move: (xx _ nB) => [[_]]. move: (ordinal_setI neR osR); set t := intersection R. move=> /funI_P [n nB nv]; move: (xx _ nB). have hsi: inc (h (csucc n)) R. by apply /funI_P;exists (csucc n) => //; apply:NS_succ. move: (setI_s1 hsi); rewrite -/t nv. move => th /oltP0 [oh _ ih]. by move: (ordinal_irreflexive oh (th _ ih)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)