proposition: Lemma CNF_prod_pr5 x y: cnfp_nz x -> cnfp_nz y -> \0o <o oexp y \0c -> (cnf_val x) *o (cnf_val y)= cnf_val (cnf_shift_expo y (cnf_degree x)).
proof: Proof. move=> xnz ynz vp. rewrite (CNF_prod_pr4 xnz ynz vp). by rewrite (CNF_prod_pr0 (proj1 ynz)(OS_cnf_degree xnz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)