proposition: Lemma cnfp_cnf_nm_range x y: cnfp x -> cnfp y -> range (cnf_nm x y) = (range x) \cup (range y).
proof: Proof. move => ha hb. set z := (cnf_nm x y). have fgz: fgraph z by rewrite /z/cnf_nm; fprops. have dz: domain z = domain x +c domain y by rewrite /z/cnf_nm; aw. move:(ha)(hb) =>[fgx nN _ _ ][fgy mN _ _]. have nmN := NS_sum nN mN. set_extens t. move/(range_gP fgz) =>[i]; rewrite dz => lis->; move/(NltP nmN):(lis) => lid. rewrite /z/cnf_nm/cnf_m LgV//. case: (cleT_el (CS_nat nN) (proj31_1 lid)) => cp1. rewrite (Y_false (cleNgt cp1)); apply: setU2_2;apply: (inc_V_range fgy). apply/(NltP mN); apply:(cdiff_Mlt mN (NS_lt_nat lid nmN) cp1). by rewrite csumC. by Ytac0; apply: setU2_1; apply: (inc_V_range fgx); apply/NltP. move => h; apply/(range_gP fgz); rewrite dz. rewrite /z/cnf_nm/cnf_m. case/setU2_P: h. move/(range_gP fgx) => [i /(NltP nN) idx ->]. have idd: inc i (domain x +c domain y). apply/(NltP nmN); apply: (clt_leT idx); apply:(csum_M0le _ (CS_nat nN)). by ex_tac; rewrite LgV//; Ytac0. move/(range_gP fgy) => [i /(NltP mN) idx ->]. have sd: inc (i +c (domain x)) (domain x +c domain y). by apply/(NltP nmN); rewrite csumC; apply:(csum_Meqlt nN idx). move:(cleNgt(csum_M0le i (CS_nat nN))); rewrite csumC => ll. by ex_tac; rewrite LgV//; Ytac0; rewrite (cdiff_pr1 (NS_lt_nat idx mN) nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)