proposition: Lemma cnf_ncms_prop x y k: cnfp x -> cnfp_nz y -> k <c (domain x) -> oexp x k = cnf_degree y -> x +f y = cnf_ncms x y k.
proof: Proof. move =>ox ynz lkn dv. move:(proj1 ynz) => oy. move: (cnfp_sum ox oy)=> oz1. have nN := proj42 ox. have mN := proj42 oy. set c := ocoef x k. move:(NS_lt_nat lkn nN) => kN. move/(cleSltP kN):(lkn) => leskn. move:(cnf_size_nz ynz)(cnf_size_nz_bis ynz). set sy := cnf_size y; move => [dyN dyv] dyl1. have sdy: sy <c (domain y) by apply/(NltP mN). have cN: natp c. move/(NltP nN): lkn => kdx. move/cnfpP: ox => /proj43 =>h; exact: (proj1 (proj33 (h _ kdx))). move: (cnf_nc_prop ynz cN) => [os1 qb qc qd qe]. have eq2: cnf_degree (cnf_nc y c) = cnf_degree y. by rewrite/cnf_degree /cnf_size qb qc. have os2:= (cnfp_cnf_ns ox leskn). have lt1: cnf_all_smaller (cnf_nc y c) (cnf_ns x (csucc k)). apply:(cnf_all_smaller_prop os1 os2). case: (equal_or_not (csucc k) (domain x)) => lt1. by constructor 2; rewrite /cnf_ns lt1 cdiff_nn /Lg funI_set0. have qq: csucc k <c domain x by split. have qa: inc \0c (domain x -c csucc k). apply/(NltP (NS_diff (csucc k) nN)); apply:card_ne0_pos; fprops. by apply: cdiff_nz. constructor 3. rewrite /cnf_ns /cnf_s/oexp LgV // (csum0l (CS_succ _)) eq2 - dv. by apply: (CNF_exponents_sM nN (proj1 (proj44 ox)) (cltS kN) qq). apply: (cnf_same_range (cnfp_sum ox (proj1 ynz)) (cnfp_cnf_nm os1 os2 lt1)). rewrite (cnfp_cnf_nm_range os1 os2). have Hu: fgraph (cnf_nc y c) by rewrite /cnf_nc; fprops. have eq3: Vg (cnf_nc y c) sy = J (cnf_degree y) (Vr x (cnf_degree y) +c Vr y (cnf_degree y)). move/(NltP nN): lkn => kdx. rewrite - (cnf_coef_of_lc ynz). rewrite -{2} dv (Vr_correct ox kdx). by rewrite /cnf_nc /cnf_c/sy LgV//; Ytac0. move:(NS_diff (csucc k) nN) => dkN. set_extens t. move => /(cnf_sum_rangeP ox ynz) => h; apply/setU2_P; case:h. - move => [ta tle]; left. move: tle;move/(range_gP (proj41 oy)):ta => [i idy ->] tl2. apply/(range_gP (proj41 os1)); rewrite qb; ex_tac; rewrite qd //. split; first by apply/(cltSleP dyN); rewrite - dyv; apply/(NltP mN). by move => ne1; case: (proj2 tl2); rewrite ne1. - move => [ty tle]; right. move: tle; rewrite - dv. move/(range_gP (proj41 ox)): ty => [i idx ->] => lt2. move:(NS_inc_nat nN idx) => iN. case: (NleT_el iN kN) => lik. case:(oleNgt (CNF_exponents_M nN (proj1 (proj44 ox)) lik lkn) lt2). move/(cleSltP kN): lik => lik. move/(NltP nN): idx => idx. have ii: inc (i -c (csucc k)) (domain x -c csucc k). apply/(NltP dkN); apply: (cdiff_pr7 lik idx nN). apply/(range_gP (proj41 os2)); rewrite /cnf_ns/cnf_s Lgd. by ex_tac; rewrite LgV //csumC cdiff_pr. - move ->; left; rewrite - eq3; apply: (inc_V_range (proj41 os1)). by rewrite qb. move=> h; apply/(cnf_sum_rangeP ox ynz). case/setU2_P: h. move/(range_gP Hu) => [i idx ->]. move: idx; rewrite qb => idy. move/(NltP mN): (idy); rewrite dyv; move/(cltSleP dyN). case/cle_eqVlt => cisy. constructor 3; rewrite cisy; apply:eq3. move:(CNF_exponents_sM mN (proj1 (proj44 oy)) cisy sdy) => hv. constructor 1. rewrite (qd _ cisy);split => //. by apply: (inc_V_range (proj41 oy)). move/(range_gP (proj41 os2)) => [i]. rewrite /cnf_ns Lgd => lid;rewrite LgV ///cnf_s => ->. move/(NltP dkN):lid => lt2. move:(csum_Meqlt (NS_succ kN) lt2); rewrite (cdiff_pr leskn) csumC => l1. constructor 2; split. by apply:(inc_V_range (proj41 ox)); apply/NltP. rewrite - dv; apply:(CNF_exponents_sM nN (proj1 (proj44 ox)) _ l1). rewrite (csum_nS _ kN); apply/(cltSleP (NS_sum (NS_lt_nat lt2 dkN) kN)). apply: (csum_Mle0 _ (CS_nat kN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)