proposition: Lemma OS_degree_aux x: ordinalp x -> x <> \0o -> ordinalp (oexp (the_CNFB x) (cnf_size (the_CNFB x))).
proof: Proof. move => /the_CNF_p0 [sa sb] xnz. move: sa => [p1 p2 p3 p4]. case (equal_or_not (domain (the_CNFB x)) \0c) => nz. by move:xnz; rewrite - sb /CNFBv nz /CNFbvo CNFq_p2. move: (p4) => [[_ p12 _ _] _]; apply: p12. rewrite /cnf_size. move:(cpred_pr p2 nz) => [mN eq]; rewrite {2} eq; apply: (cltS mN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)