proposition: Lemma CNF_sum_pr3 x y: cnfp_nz x -> cnfp_nz y -> cnf_degree x = cnf_degree y -> cnf_val x +o cnf_val y = cnf_val(cnf_nc y (cnf_lc x)).
proof: Proof. move => xnz ynz sd. rewrite - (cnf_ncms_prop_sd xnz ynz sd). by rewrite (cnf_sum_compat_prop (proj1 xnz) (proj1 ynz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)