proposition: Lemma nsv_aux u d: \0o <o u -> odegree u <=o d -> exists c r, [/\ c <o omega0, r <o oopow d & u = oopow d *o c +o r].
proof: Proof. move => up /ole_eqVlt; case => dxy. move/the_cnf_split:up; move => [ha hb hc hd]; rewrite - dxy. by exists (the_cnf_lc u), (the_cnf_rem u). exists \0o, u; split. - apply:olt_0omega. - by apply:(olt_leT (proj2 (the_cnf_p4 up))); apply: opow_Mo_le;apply/oleSltP. - by rewrite oprod0r (osum0l (proj32_1 up)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)