proposition: Lemma the_CNF_p0 x (X:= the_CNFB x): ordinalp x -> CNFB_ax X /\ CNFBv X = x.
proof: Proof. move => ox. suff: (CNFB_ax X /\ CNFBv X = x) /\ inc X (CNFB_bound x) by move => []. apply: select_pr. move: (CNFB_exists ox) => [z za zb]; exists z => //. by rewrite - zb ; apply:CNFB_bound_p. move => a b' _ [p1 p2] _ [p3 p4]. rewrite - p4 in p2;exact:(CNFB_unique p1 p3 p2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)