proposition: Lemma CNFB_e_p2 x (E := CNFB_expos x): ordinalp x -> (finite_set E /\ ordinal_set E).
proof: Proof. move => ox. move:(the_CNF_p0 bg2 ox) => [[fgz nN pz ax] _]. have aux: cardinal E = domain (the_CNFB b x). rewrite (CNFB_card_range ox). by apply: cardinal_fun_image; move: (proj2 (CNFB_range_fgraph ox)). split. by apply/NatP; rewrite aux. move => t /funI_P [z /(range_gP fgz) [i idy ->]->]. by apply: (proj42 (proj1 ax));apply/(NltP nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)