proposition: Lemma CNFB_e_p4 x: ordinalp x -> (forall y, inc y (CNFB_expos x) -> y <=o x).
proof: Proof. move => ox y. case: (ozero_dichot ox) => xz. by rewrite xz CNFB_expos_zero => /in_set0. move:(the_CNF_p0 bg2 ox) => [[fgz nN zp ax] sv]. move:(the_CNF_p2 bg2 xz) => []; set m := cnf_size _ => mN mv. move/funI_P =>[z /(range_gP fgz) [i idz -> ] ->]. rewrite mv in idz ax; move /(NleP mN): idz => lim. move: (CNF_exponents_M (NS_succ mN) (proj1 ax) lim (cltS mN)) => le1. by move: (oleT le1 (CNFB_e_p3 mN ax)); rewrite - mv -/(CNFBv b _) sv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)