proposition: Lemma cnf_sum_prop6 x c: cnfp_nz x -> natp c -> cnf_val (cnf_nc x c) = oopow (cnf_degree x) *o c +o (cnf_val x).
proof: Proof. move => xnz cN. move:(cnf_nc_prop xnz cN); set z := cnf_nc _ _. move => [oz dz zexp zg zlc]. move:(cnf_size_nz xnz)(cnf_size_nz_bis xnz). set m := cnf_size x; move => [mN dxv] hh. have co: c <o omega0 by apply olt_omegaP. move:(proj44 (proj1 xnz));rewrite /cnf_val dxv => axo. move: (CNFb_change_nv mN axo co) => [ha <-]. rewrite dz - dxv; apply: (osumf_exten (proj42 (proj1 xnz))) => i ilx. move/(NltP (proj42 (proj1 xnz))): (ilx) => idx. rewrite /cantor_mon (zexp _ ilx) /z/cnf_nc /ocoef/cnf_c LgV//; apply: f_equal. by Ytac h; Ytac0; aw; trivial;rewrite (osum2_2int cN (proj1 (posnat_lc xnz))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)