proposition: Lemma cnf_sd_lc x y : cnfp_nz x -> cnfp_nz y -> cnf_degree x = cnf_degree y -> cnf_lc(x +f y) = (cnf_lc x) +c cnf_lc y.
proof: Proof. move => xnz ynz sd. rewrite(cnf_ncms_prop_sd xnz ynz sd). have cN:= (proj1 (posnat_lc xnz)). by move: ( (cnf_nc_prop ynz cN)) =>[_ _ _ _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)