proposition: Lemma nds_fL_prop6 v (X2:= (fun z => X (k +c z))): inc v (nds_sums X n) -> exists v1 v2, [/\ inc v1 (nds_tn_S X k), inc v2 (nds_sums X2 (n -c k)) & v = v2 +o v1].
proof: Proof. move => /funI_P [z zp ->]. move: (nds_fL_prop5 zp) => [K [s1 [s2 [/setP_P pa pb pc ->]]]]. set v1:=nds_sc (fun z0 => X (nth_elt K z0)) (cardinal K) s1. set v2:=nds_sc (fun z => X (k +c z)) (n -c k) s2. have v2p:inc v2 (nds_sums X2 (n -c k)) by apply/funI_P; ex_tac. exists v1, v2; split => //;apply/setUf_P; ex_tac; apply/funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)