proposition: Lemma the_cnf_p4 x (n := odegree x): \0o <o x -> oopow n <=o x /\ x <o oopow (osucc n).
proof: Proof. move => xp; rewrite /n (odegree_of_pos xp). move: (the_cnf_p2 xp) => []; set m := cnf_size _; move => mN mv. move: xp => [[ _ ox _] xnz]. move:(the_cnf_p0 ox) => [[_ nN _ ax] sb]. rewrite mv in ax; split. by move:(CNFq_pg4 mN ax);rewrite -mv -/CNFbvo -/(cnf_val _) sb. move:(CNFq_pg1 mN (proj1 ax));rewrite -mv -/CNFbvo -/(cnf_val _) sb //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)