proposition: Lemma cnf_ncms_prop_sd x y : cnfp_nz x -> cnfp_nz y -> cnf_degree x = cnf_degree y -> x +f y = cnf_nc y (cnf_lc x).
proof: Proof. move => xnz ynz sd. have ox := proj1 xnz. move: (cnf_size_nz xnz) => [mN mv]. move/(NltP (proj42 ox)):(cnf_size_nz_bis xnz) => mk. rewrite (cnf_ncms_prop ox ynz mk sd) /cnf_ncms -/(cnf_lc x) - mv. have ->: (cnf_ns x (domain x)) = emptyset. rewrite /cnf_ns cdiff_nn; apply: funI_set0. have cN:= (proj1 (posnat_lc xnz)). move: (cnf_nc_prop ynz cN). set u := cnf_nc _ _; move => [pa pn pc pd pe]. have dd1: domain u +c emptyset = domain u. by rewrite (csum0r (CS_nat (proj42 pa))). have sdd: domain (cnf_nm u emptyset) = domain u by rewrite /cnf_nm Lgd; aw. apply: fgraph_exten. - rewrite /cnf_nm; fprops. - exact (proj41 pa). - exact. - rewrite sdd => i idu; rewrite /cnf_nm domain_set0 dd1 LgV//. by rewrite /cnf_m Y_true //; apply/(NltP (proj42 pa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)