proposition: Lemma the_cnf_omega_kj j k (X := omega0 *o j +o k): posnatp j -> natp k -> \0o <o X /\ [/\ odegree X = \1o, the_cnf_lc X = j & the_cnf_rem X = k].
proof: Proof. move => pnj kN. have ok := (OS_nat kN). move/posnat_ordinalp: (pnj) => [jp jlo]. have lt0:= (oprod2_pos olt_0omega jp). have xp: \0o <o X. apply: (olt_leT lt0 (osum_Mle0 (proj32_1 lt0) ok)). rewrite (odegree_of_pos xp). split; first exact. case: (czero_dichot (CS_nat kN)) => kz. have cp1: inc (cpred \1c) \1c by rewrite cpred1; apply: (set1_1 \0c). rewrite /X kz(osum0r (proj32_1 lt0)) - oopow1. move: (cnf_one_term OS1 pnj)=> [qa qb qc qd]. rewrite /the_cnf_lc /the_cnf_rem qc /cnf_lc /cnf_rem/cnf_size. aw; rewrite /oexp/ocoef ! LgV//; aw. by rewrite cpred1 /CNFbvo /CNFbv osum_f0. have ->: X = oopow \1o *o j +o oopow \0c *o k. by rewrite oopow0 oopow1 (oprod1l ok). move: (cnf_two_terms olt_01 pnj (conj kN kz)) => [qa qb qc qd]. rewrite /the_cnf_lc /the_cnf_rem qc /cnf_lc /cnf_rem/cnf_size; aw. rewrite cpred2 /CNFbvo /CNFbv - {3} succ_zero (osum_fS _ NS0) osum_f0. rewrite /ocoef /oexp /cantor_mon; aw. by rewrite opowx0 (oprod1l ok) (osum0r ok). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)