proposition: Lemma CNF_pow_pr2 x k: omega0 <=o x -> posnatp k -> odegree (x ^o k) = (odegree x) *o k /\ oleading_coef(x ^o k) = oleading_coef x.
proof: Proof. move => xinf [ka /proj2/nesym kb]. move:(olt_leT olt_0omega xinf) => xnz. move:(proj32_1 xnz) => ox. move:(OS_degree ox) => od. move:(cpred_pr ka kb) =>[nN ->]. move: (cpred k)nN; clear k ka kb. apply: Nat_induction. by rewrite succ_zero (opowx1 ox) (oprod1r od). move => n nN [ha hb]. move:(OS_nat (NS_succ nN)) => osn. rewrite(succ_of_nat (NS_succ nN)) (opow_succ ox osn). move: (opow_pos xnz osn) => xpnz. rewrite (odegree_prod xpnz xnz) (oleading_coef_prod2 xpnz xinf). by rewrite ha - oprod2_succ. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)