proposition: Lemma the_cnf_split x (e:= odegree x) (c:= the_cnf_lc x) (r := the_cnf_rem x): \0o <o x -> [/\ \0o <o c, c <o omega0, r <o oopow e & x = oopow e *o c +o r].
proof: Proof. move => xp. move:(the_cnf_p2 xp); rewrite /e /c/r (odegree_of_pos xp). set m := cnf_size _; move => [mN Pv]. move: (the_cnf_p0 (proj32_1 xp)) => [[_ nN _]]. rewrite /CNFBv Pv. move => sb sc. move: (sb) => [[a1 a2 a3 a4] a5]. split. + exact:(a5 _ (cltS mN)). + exact:(a3 _ (cltS mN)). + exact:(CNFq_pg mN (proj1 sb)). + by rewrite -{1} sc /cnf_val Pv - (CNFq_p1 _ _ _ mN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)