proposition: Lemma CNFr_exists_aux x: \0o <o x -> exists n y, [/\ ordinalp n, y <o x , y <o oopow n *o omega0 & x = oopow n +o y].
proof: Proof. move => xp. move: (ord_ext_div_exists ole_2omega xp) =>[e1 [c1 [rm [oe1 oc1 or [eq1 lt1 lt2 lt3]]]]]. move: (ord_rev_pred lt3); set c2 := (c1 -o \1o); move => [oc2 eql]. have eql2: c1 = c2 +o \1o. move: (osum_M0le OS1 oc2);rewrite - eql => h; move: (ole_ltT h lt2) => aa. have c2N: natp c2 by apply:(olt_i aa). by move: eql; rewrite (osum2_2int NS1 c2N) csumC - (osum2_2int c2N NS1). set q := (omega0 ^o e1); set rm1 := ((q *o c2) +o rm). have oq:= proj32_1 lt1. have op2: ordinalp (q *o c2) by fprops. have orm1: ordinalp rm1 by rewrite /rm1; fprops. move: OS_omega OS1 => oo o1. have yv1: x = q +o rm1 by rewrite eq1 eql oprodD // oprod1r // /rm1 osumA. have pv2: q *o c1 = (q *o c2) +o q by rewrite eql2 oprodD // oprod1r //. have yv2: x = (q *o c2) +o (q +o rm) by rewrite eq1 pv2 osumA //. have rmy: rm1 <o x. split; first by rewrite yv1; apply: osum_M0le. rewrite /rm1 yv2 => eq3. move: (osum_Mle0 oq or);rewrite - (osum2_simpl or (OS_sum2 oq or) op2 eq3). by move => /(oleNgt) []. have lt: rm1 <o omega0 ^o e1 *o omega0. apply: olt_leT (oprod_Meqle (proj1 lt2) oq). rewrite pv2; exact: (osum_Meqlt lt1 op2). by exists e1, rm1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)