proposition: Lemma cnf_sum_prop5 x: cnfp_nz x -> cnf_val x = (oopow (cnf_degree x)) *o (cnf_lc x) +o (cnf_rem x).
proof: Proof. move => xnz. move: (cnf_size_nz xnz) => [qa qb]. by rewrite /cnf_val /cnf_rem qb /CNFbvo /CNFbv (osum_fS _ qa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)