proposition: Lemma ovaluation6 x: \0o <o x -> exists2 z, osuccp z & x = oopow (ovaluation x) *o z.
proof: Proof. move => xp. move:(the_cnf_p0_nz xp); set y := the_cnf x; move=> [ynz yv]. have oy := proj1 ynz. rewrite/ovaluation;move. move: (cnf_size_nz ynz); set m := cnf_size y; move => [mN mv]. set v := oexp y \0c. set z := Lg (domain y) (fun i => J ( (oexp y i) -o v) (ocoef y i)). have nN := (proj42 oy). have Ha k: k <c domain y -> v <=o oexp y k. move => lkn; move:(cle0x (proj31_1 lkn)) => kp. exact: (CNF_exponents_M nN (proj1 (proj44 oy)) kp lkn). have Hb1 k: k <c (domain y) -> oexp z k = (oexp y k) -o v. by move => /(NltP nN) kdx ; rewrite/z/oexp LgV//; aw. have Hb k: k <c (domain y) -> ordinalp (oexp z k) /\ oexp y k = v +o (oexp z k). move => kdx; rewrite (Hb1 _ kdx); exact: (odiff_pr (Ha _ kdx)). have ody:= (proj1(cnf_size_nz_ter ynz)). have ov: ordinalp v. by move/cnfpP: oy => /proj43 h; case : (h _ ody). have oz: cnfp z. rewrite/z; move/cnfpP:oy =>[ha hb hc hd]; apply/cnfpP; split. - fprops. - by aw. - aw =>i idy;rewrite LgV //; move:(hc i idy) =>[qa qb qc]; split; aww. have ->: (oexp y i -o v) = oexp z i by rewrite /z/oexp LgV//; aw. by move/(NltP hb): idy => /Hb/proj1. - aw;move => i iN lin. move: (clt_ltT (cltS iN) lin) => liin. move: (Hb _ lin) (Hb _ liin) =>[oe1 -v1][oe2 v2]. apply:(osum_Meqltr oe2 oe1 ov); rewrite - v1 - v2; exact: (hd i iN lin). move:(cnf_and_val_pb oz) =>[]; set t := cnf_val z. move => _ ot zv _. have ovt: ovaluation t = \0o. by rewrite /ovaluation zv /z/oexp LgV//; aw; rewrite (odiff_wrong (oleR ov)). have xv: x = oopow v *o t. rewrite -(CNF_prod_pr0 oz ov) - yv; rewrite/cnf_val/CNFbvo /CNFbv. have dz: domain z = domain y by rewrite /z Lgd. have ->: (domain (cnf_shift_expo z v)) = domain y. rewrite /cnf_shift_expo Lgd//. apply: (osumf_exten nN) => i ily;rewrite /cantor_mon/oexp /ocoef. move/(NltP nN): (ily) => idy; move:(idy); rewrite - dz => idz. rewrite /cnf_shift_expo LgV//; aw. by rewrite -(proj2 (Hb _ ily)) /z /ocoef LgV//; aw. have tp: \0o <o t. by apply: (ord_ne0_pos ot) => tz; case: (proj2 xp); rewrite xv tz oprod0r. move: (ovaluation2 tp ovt) => ost. by rewrite xv; exists t. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)