proposition: Lemma nds_card_merge n k Y: natp n -> k <c n -> opos_below Y (n -c k) -> nds_card (nds_merge k Y) n = ndsC k *c nds_card Y (n -c k).
proof: Proof. move => nN kln Yp. have kN := NS_lt_nat kln nN. have nkN := NS_diff k nN. move: (cdiff_pr (proj1 kln)) => dv. have Xpb:= OS1. set X := (nds_merge k Y). have xsi i: i <c k -> X i = nds_base i by rewrite /X /nds_merge=> h; Ytac0. have gxi i: i <c n -c k -> X (k +c i) = nds_shift (Y i). move => /proj31_1 ic. rewrite /X /nds_merge (Y_false (cleNgt (csum_M0le i (CS_nat kN)))). by rewrite csumC (cdiff_pr1' ic kN). move: (nds_merge_prop2 kN nkN Yp) => [Xpc Xpd]; rewrite dv in Xpd. rewrite - (nds_tn_ex_val kN). have <-: nds_tn_C (nds_merge k Y) k = nds_tn_C nds_base k. by apply: (nds_tn_C_exten kN) => i /xsi. set E := (nds_sums (fun z => X (k +c z)) (n -c k)) . have aux: forall i, inc i (nds_tn_S X k) -> nds_binomp i. move => i /setUf_P [K /setP_P K1 /funI_P [s sp] ->]. have sKN:= (sub_trans K1 (NS_inc_nat kN)). have fsk:= (sub_finite_set K1 (finite_set_nat kN)). have cKN: natp (cardinal K) by apply /NatP. have : forall i, i <c (cardinal K) -> nds_binomp (X (nth_elt K (Vf s i))). move => j jk. have r0: (Vf s j) <c cardinal K. move /permutationsP: sp => [[[fs _] _] ss ts]. by apply/(NltP cKN); Wtac; rewrite ss; apply/(NltP cKN). have r1:(nth_elt K (Vf s j)) <c k. apply /(NltP kN); apply:K1; apply: nth_elt_inK => //. apply: (NS_lt_nat r0 cKN). rewrite (xsi _ r1); exact: (nds_binomp_base (NS_lt_nat r1 kN)). rewrite /nds_sc_Ktau/nds_sc. move: (cardinal K) cKN; apply: Nat_induction. by move => _; rewrite osum_f0; apply: (oopow_pos OS2). move => m mN Hrec /(true_below_rec mN) [a1 a2]. rewrite /nds_sc (osum_fS _ mN); apply: (nds_binomp_add a2 (Hrec a1)). have aux2: forall i j u v, inc i (nds_tn_S X k) -> inc j (nds_tn_S X k) -> inc u E -> inc v E -> u +o i = v +o j -> (u = v /\ i = j). move => i j u v ia ja /funI_P [s1 s1p v1p] /funI_P [s2 s2p v2p]. move/permutationsP:s1p => [[[fs1 _] _] sf1 tf1]. move/permutationsP:s2p => [[[fs2 _] _] sf2 tf2]. have ha: forall q, q<c n -c k -> (Vf s1 q) <c n -c k. by move => q qa;apply /(NltP nkN); Wtac; rewrite sf1; apply/(NltP nkN). have hb: forall q, q<c n -c k -> (Vf s2 q) <c n -c k. by move => q qa;apply /(NltP nkN); Wtac; rewrite sf2; apply/(NltP nkN). have v1a: u = nds_sc (fun z => nds_shift (Y z)) (n -c k) s1. by rewrite v1p; apply:(osumf_exten nkN) => q /ha /gxi. have v2a: v = nds_sc (fun z => (nds_shift (Y z))) (n -c k) s2. by rewrite v2p; apply:(osumf_exten nkN) => q /hb/gxi. have ax1: nds_ax (fun z => Y (Vf s1 z)) (n -c k). by move => z /ha/Yp /proj32_1. have ax2: nds_ax (fun z => Y (Vf s2 z)) (n -c k). by move => z /hb/Yp /proj32_1. move:(osum_shift nkN ax1) (osum_shift nkN ax2) => [qa qb][qc qd]. rewrite v1a v2a /nds_sc qb qd => eq1; move:(nds_add_sb_inj qa qc(aux i ia) (aux j ja) eq1). move => [-> ->]; split; reflexivity. pose F a :=(fun_image E (osum2^~ a)). have H: forall a, inc a (nds_tn_S X k) -> cardinal (F a) = nds_card Y (n -c k). move => a ias. have xx: nds_ax Y (n -c k) by move => t /Yp /proj32_1. rewrite cardinal_fun_image. rewrite (nds_card_shift nkN xx). by apply:(nds_card_exten nkN) => i /gxi. move => u v ua va /= eq; exact: (proj1 (aux2 _ _ _ _ ias ias ua va eq)). have hu: nds_type_nor X n k \1c. move:(nds_merge_prop1 kN nkN Yp); rewrite dv => hu. split => //; split; first by move => i /hu [qa qb]. exists \1c; split => //. move => i lin; case:(cleT_el (CS_nat kN) (proj31_1 lin)) => cp. exact: (proj1(Xpd i cp lin)). by rewrite (Xpc i cp); apply: oleR. set Z := Zo _ _. suff: Z = k by move ->; apply: card_nat. set_extens t. move=> /Zo_P [/(NltP nN) ltn dt1]. case:(cleT_el (CS_nat kN) (proj31_1 ltn)) => cp; last by apply/(NltP kN). by move:(proj2(Xpd t cp ltn)); rewrite dt1. move/(NltP kN) => ltk; apply: Zo_i (Xpc _ ltk). by move/(NltP nN): (clt_ltT ltk kln). rewrite /nds_card (nds_tg9 nN kln hu) csum_pr4_bis. rewrite cprodC /nds_tn_C cprod2cr - csum_of_same /csumb. by apply: f_equal; apply: Lg_exten => i ib; apply: H. move => i j ia ja; case (equal_or_not i j) => eij; [by left | right]. apply:disjoint_pr => u /funI_P [v1 va vb] /funI_P [v2 vc vd]. rewrite vb in vd; case eij; exact: (proj2 (aux2 _ _ _ _ ia ja va vc vd)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)