proposition: Lemma CNF_sum_pr2 x y n: cnfp x -> cnfp_nz y -> n <c (domain x) -> oexp x n = cnf_degree y -> cnf_val x +o cnf_val y = cnf_val(cnf_ncms x y n).
proof: Proof. move => ox ynz lnd ha. rewrite - (cnf_ncms_prop ox ynz lnd ha). by rewrite (cnf_sum_compat_prop ox (proj1 ynz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)