proposition: Lemma cnfp_cnf_mergeK x k : cnfp x -> k <=c domain x -> cnf_nm (cnf_nr x k) (cnf_ns x k) = x.
proof: Proof. move => ox le1. rewrite /cnf_nm/cnf_m. have ->: domain (cnf_nr x k) = k by rewrite /cnf_nr Lgd. have ->: domain (cnf_ns x k) = (domain x -c k) by rewrite /cnf_ns Lgd. symmetry;rewrite (cdiff_pr le1). move: (ox) => [fgx nN _ _]; apply: fgraph_exten; [ exact | fprops | by aw | ]. move => i /= idx; rewrite (LgV idx); move/(NltP nN): idx => idx. case: (cleT_el (proj31 le1) (proj31_1 idx)) => cp1. have aux: inc (i -c k) (domain x -c k). by apply/(NltP (NS_diff k nN));apply:cdiff_pr7. rewrite (Y_false (cleNgt cp1)) /cnf_ns/cnf_s LgV//. by rewrite csumC (cdiff_pr cp1). by Ytac0; rewrite /cnf_nr LgV//; apply/(NltP (NS_le_nat le1 nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)