proposition: Lemma CNF_prod_pr2 x : cnfp_nz x -> cnf_val x *o omega0 = oopow (cnf_degree x) *o omega0.
proof: Proof. move=> xnz. have od:= OS_cnf_degree xnz. have h4:= (OS_oopow od). have h5:= OS_prod2 h4 OS_omega. apply: oleA; last first. rewrite (cnf_sum_prop5 xnz); apply: (oprod_Mleeq _ OS_omega). move/posnat_ordinalp: (posnat_lc xnz) => [pa _]. move: (OS_prod2 h4 (proj32_1 pa)) => h6. apply: (oleT (oprod_Mle1 h4 pa)). apply: (osum_Mle0 h6 (OS_cnf_rem (proj1 xnz))). have pc':= (OS_cnf_valp xnz). have ov := proj32_1 pc'. move: (oprod_normal pc') => [pg pk]. rewrite (pk _ (omega_limit)); clear pk. apply: ord_ub_sup => //. move=> i /funI_P [z zo ->]. move: zo => /(oltP OS_omega) zo. have oz:= proj31_1 zo. case: (ozero_dichot oz) => zno. by rewrite zno (oprod0r); apply: ole0x. move: (cnf_size_nz xnz) => [qa qb]. move: (proj44 (proj1 xnz)) => axo. move: (cnf_size_nz_bis xnz) => sd1. move /(NltP (proj42 (proj1 xnz))):(sd1) => sd. move: (axo) => [[_ h1 h2 _] h3]. move: (oprod2_lt_omega (h2 _ sd) zo) => /oleSltP so. have pnz: posnatp z by apply/posnat_ordinalp. rewrite (@CNF_prod_pr1 x z xnz pnz). rewrite /cnf_val/CNFbvo {3}/cnf_nck Lgd qb (CNFq_p1 _ _ _ qa). rewrite {1 2} /cnf_nck /cantor_mon /oexp/ocoef/cnf_c LgV//; Ytac0; aw. set w := CNFbv _ _ _ _. have lt1: w <o omega0 ^o (oexp x (cnf_size x)). move: (pnz) => [za zb]; move: (cpred_pr za (nesym (proj2 zb))) => [zc zd]. move: (proj44 (cnf_nck_prop3 xnz zc)); rewrite - zd. move/ proj1; rewrite {3}/cnf_nck Lgd qb => ax1. apply:(CNFq_pg3 qa (CNFq_p5 qa ax1) (h1 _ sd)). have aux: cnf_size x <c csucc (cnf_size x) by rewrite - qb. move => k kn. move: (CNF_exponents_sM (NS_succ qa) ax1 kn aux). by rewrite {2} /cnf_nck {2}/oexp /cnf_c LgV//; Ytac0; aw. have oy1 := (OS_prod2 (proj32_1 (proj2 (proj44 (proj1 xnz)) _ sd)) oz). have hh4:= (OS_prod2 h4 oy1). move: (osum_Meqlt lt1 (OS_prod2 h4 oy1)); rewrite - (oprod2_succ h4 oy1). have eq0: (ocoef x (cnf_size x) *o z) = (cnf_lc x *c z). rewrite -/(cnf_lc _). by rewrite (oprod2_2int (proj1 (posnat_lc xnz)) (proj1 pnz)). rewrite {1} eq0. move => [le1 _]; apply: (oleT le1 (oprod_Meqle so h4)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)