proposition: Lemma the_cnf_omega_k k (X := omega0 +o k): natp k -> [/\ \0o <o X, odegree X = \1o & the_cnf_rem X = k].
proof: Proof. move => kN. move:(the_cnf_omega_kj PN1 kN ). by rewrite (oprod1r OS_omega); move => [ra [rb rc rd]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)