proposition: Lemma the_cnf_p5 e c n (x:= CNFbvo e c (csucc n)): natp n -> CNFb_axo e c (csucc n) -> \0o <o x /\ odegree x = e n.
proof: Proof. move => nN ax. move:(CNFq_pg5 nN ax) => xp. split; first by exact. rewrite (odegree_of_pos xp). move:(the_cnf_p2 xp). rewrite(the_cnf_p3 ax (NS_succ nN)). set m := cnf_size _. rewrite Lgd; move => [mN mm]. rewrite (csucc_inj (CS_nat nN) (CS_nat mN) mm) /oexp LgV//; aw; trivial. exact (Nsucc_i mN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)