proposition: Lemma ovaluation1 x: \0o <o x -> exists2 y, ordinalp y & x = y +o oopow (ovaluation x).
proof: Proof. move => xp. move: (the_cnf_p0 (proj32_1 xp)) => [ax0 xv]. move: (ax0) (the_cnf_p2 xp) => [_ pb _ ax] [nN pc]. rewrite /ovaluation -{1} xv /CNFBv. rewrite pc in ax. move:(CNFb_Al nN ax)=> [oc3 ax3]; rewrite - pc /cnf_val => ->. set y := CNFbvo _ _ _. rewrite /cantor_mon. set a := oexp _ _; set b := ocoef _ _. have oy: ordinalp y by apply:OS_CNFb. move:ax => [[_ h1 h2 _] h3]. have lt0:=(succ_positive (cnf_size (the_cnf x))). move:(h1 _ lt0) (h2 _ lt0)(h3 _ lt0); rewrite -/a -/b => oa /olt_omegaP bN bp. have [/proj32 ob /nesym bnz]:= bp. have ooa:ordinalp (omega0 ^o a). by fprops. move: (cpred_pr bN bnz) =>[np ->]; move:(OS_nat np) => op. have ooc:= (OS_prod2 ooa op). rewrite (succ_of_nat np) (oprod2_succ ooa op) (osumA oy ooc ooa). exists (y +o omega0 ^o a *o cpred b) => //; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)