proposition: Lemma cnf_sum_prop8 x y (d := cnf_degree y) (k := position_in_cnf x d): cnfp x -> cnfp_nz y -> x +f y = cnf_sum (cnf_ns x k) y.
proof: Proof. move => ox ynz. move: (OS_cnf_degree ynz); rewrite -/d => od. move: (position_in_cnf_prop ox od); rewrite -/k. move => [kdx kp1 kp2]. move: (cnfp_cnf_ns ox kdx) => oz. have nN := proj42 ox. have kN := NS_le_nat kdx nN. have aux: Vr (cnf_ns x k) d = Vr x d. case: (inc_or_not d (domain (range x))) => ddrx. move/funI_P:ddrx => [t tx tv]; move/(range_gP (proj41 ox)):tx =>[i idx iv]. have dv: d = oexp x i by rewrite tv iv. rewrite {2} dv (Vr_correct ox idx). move/(NltP nN): (idx) => iix. move: (NS_inc_nat nN idx) => iN. case: (NleT_el kN iN) => lik; last by case:(proj2 (kp1 _ lik));ue. have sidx: inc (i -c k) (domain x -c k). by apply/(NltP (NS_diff k nN)); apply: cdiff_pr7. have idz: inc (i -c k) (domain (cnf_ns x k)) by rewrite/cnf_ns Lgd. move:(Vr_correct oz idz). rewrite {2 3} /cnf_ns/cnf_s /oexp /ocoef LgV//. by rewrite (csumC _ k) (cdiff_pr lik) dv. rewrite /Vr (Vg_out_of_range ddrx). case: (inc_or_not d (domain (range (cnf_ns x k)))) => hu; last first. by rewrite (Vg_out_of_range hu). move/funI_P:hu => [t tx tv]; move/(range_gP (proj41 oz)):tx =>[i]. rewrite /cnf_ns Lgd => idx; rewrite LgV// => iv. case: ddrx; rewrite tv iv /cnf_s; apply /funI_P. exists ((Vg x (i +c k))) => //; apply: (inc_V_range (proj41 ox)). apply/(NltP nN). move/(NltP (NS_diff k nN)): idx => lik. by move:(csum_Meqlt kN lik); rewrite (cdiff_pr kdx) csumC. apply: (cnf_same_range (cnfp_sum ox (proj1 ynz)) (cnfp_sum oz (proj1 ynz))). set_extens t. move/(cnf_sum_rangeP ox ynz) => h; apply/(cnf_sum_rangeP oz ynz). case: h. - by constructor 1. - move => [ha hb]; constructor 2; split => //. apply/(range_gP (proj41 oz)). move/(range_gP (proj41 ox)): ha =>[i idx iv]. move:hb; rewrite iv => hb. move/(NltP nN): (idx) => iix. move: (NS_inc_nat nN idx) => iN. case: (NleT_el kN iN) => lik; last by move:(oltNge hb (proj1(kp1 _ lik))). have sidx: inc (i -c k) (domain x -c k). by apply/(NltP (NS_diff k nN)); apply: cdiff_pr7. by rewrite /cnf_ns Lgd; ex_tac; rewrite LgV// /cnf_s csumC cdiff_pr. - move => tv; constructor 3; rewrite tv aux; reflexivity. move/(cnf_sum_rangeP oz ynz) => h; apply/(cnf_sum_rangeP ox ynz). case: h. - by constructor 1. - move =>[ha hb]; constructor 2; split => //. move/(range_gP (proj41 oz)): ha =>[i]. rewrite /cnf_ns /cnf_s Lgd => idx; rewrite LgV//; move ->. apply: (inc_V_range (proj41 ox)); apply/(NltP nN). move/(NltP (NS_diff k nN)): idx => lik. by move:(csum_Meqlt kN lik); rewrite (cdiff_pr kdx) csumC. - move => tv; constructor 3; rewrite tv aux; reflexivity. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)