proposition: Lemma the_CNF_p2 x (m := (cnf_size (the_CNFB x))): \0o <o x -> natp m /\ domain (the_CNFB x) = csucc m.
proof: Proof. move => [[ _ ox _] xnz]. move:(the_CNF_p0 ox) => [[_ nN _ ax] sb]. case (equal_or_not (domain (the_CNFB x)) \0c) => nz. by move:xnz; rewrite - sb /CNFBv nz /CNFbvo CNFq_p2. exact: (cpred_pr nN nz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)