proposition: Lemma CNF_pow_pr1 x k: cnfp_nz x -> \0o <o (oexp x \0c) -> natp k -> (cnf_val x) ^o (osucc k) = (oopow ((cnf_degree x) *o k)) *o (cnf_val x).
proof: Proof. move=> xp vxp. move:(OS_cnf_valp xp) => xnz;move:(proj32_1 xnz) => ox. move: (OS_cnf_degree xp) => olcx. move: k; apply: Nat_induction. by rewrite (oprod0r) oopow0 (oprod1l ox) osucc_zero opowx1. move=> k kN hrec. move:(OS_nat kN) => ok. have osk := OS_succ ok. have odf:=(OS_prod2 olcx ok). move: (OS_pow OS_omega odf)(OS_pow OS_omega olcx) => of1 ood. rewrite (succ_of_nat kN)(opow_succ ox osk) hrec -(oprodA of1 ox ox). rewrite (CNF_prod_pr4 xp xp vxp) (oprodA of1 ood ox)(oprod2_succ olcx ok). by rewrite - (opow_sum OS_omega odf olcx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)