proposition: Lemma CNF_prod_pr0 x d: cnfp x -> ordinalp d -> cnf_val (cnf_shift_expo x d) = oopow d *o (cnf_val x).
proof: Proof. move => ox od. rewrite /cnf_val/cnf_shift_expo/CNFbvo/CNFbv Lgd. move: (proj42 ox)(proj44 ox);set n := domain x => nN ax. pose e' i := d +o oexp x i. transitivity (osumf (cantor_mon omega0 e' (ocoef x)) n). apply: (osumf_exten nN) => i /(NltP nN)lin; aw. by rewrite/cantor_mon/ oexp/ocoef LgV//; aw. move: n nN ax; apply:Nat_induction; first by rewrite ! osum_f0 oprod0r. move => n nN Hrec axn. have ax:=(CNFb_p5 nN axn). have ood := (OS_oopow od). have ooe:=(OS_oopow (CNFb_p8 axn nN)). rewrite (osum_fS _ nN) (osum_fS _ nN) (Hrec ax). rewrite (oprodD (CNFq_p0 (proj1 axn) (cltS nN)) (OS_CNFb nN ax) ood). rewrite/cantor_mon (oprodA ood ooe (proj32_1(proj2 axn _ (cltS nN)))). by rewrite (opow_sum OS_omega od (CNFb_p8 axn nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)