proposition: Lemma CNF_prod_pr4 x y: cnfp_nz x -> cnfp_nz y -> \0o <o oexp y \0c -> cnf_val x *o cnf_val y = oopow (cnf_degree x) *o cnf_val y.
proof: Proof. move=> xnz ynz pnz; set Y := cnf_val y. move: (cnf_and_val_pb (proj1 ynz)) => [_ ha hb _]. move: (cnf_and_val_pb (proj1 xnz)) => [_ _ hc _]. have vp: \0o <o ovaluation Y by rewrite/ovaluation /Y hb. move:(OS_cnf_valp xnz) (OS_cnf_valp ynz) => xp Yp. move: (ovaluation3 Yp vp) => ly. rewrite(CNF_prod_pr3 xp ly) /cnf_degree. by rewrite (odegree_of_nz (nesym (proj2 xp))) hc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)