proposition: Lemma CNFB_e_p6 x (y:=CNFB_expos x): ordinalp x -> ((b_critical x -> y = singleton x) /\ (~ (b_critical x) -> forall a, inc a y -> a <o x)).
proof: Proof. move => ox. move:(the_CNF_p0 bg2 ox) => [[fgz nN pz ax] xv]. case: (ozero_dichot ox) => nz. split; first by rewrite nz /b_critical opowx0 => h; case: card1_nz. by rewrite /y nz CNFB_expos_zero => _ t /in_set0. move:(the_CNF_p2 bg2 nz) => []; set m := cnf_size _ => mN mv. rewrite mv in ax. move: (CNFB_e_p5 mN ax); rewrite -mv -/(CNFBv _ _) xv; move=> [ph pi]. have ha: inc m (domain (the_CNFB b x)) by rewrite mv; apply: Nsucc_i. split. move=> cx; move: (pi cx) => [pj pk]. pose z := (the_CNFB b x). have eq1: range z = singleton (Vg z m). apply: (set1_pr (inc_V_range fgz ha)) => u /(range_gP fgz) [i idx ->]. by move: idx; rewrite mv pj succ_zero => /set1_P ->. by rewrite /y /CNFB_expos/ cnf_exponents eq1 /domain funI_set1 - pk. move=> ncx. move: (CNFB_e_p3 mN ax); rewrite - mv -/(CNFBv _ _) xv => le1. have lt1: oexp (the_CNFB b x) m <o x by split => //; dneg h; apply: ph. move => a /funI_P [d /(range_gP fgz) [i idz ->] ->]. rewrite mv in idz ax; move /(NleP mN): idz => lim. exact:(ole_ltT (CNF_exponents_M (NS_succ mN) (proj1 ax) lim (cltS mN)) lt1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)