proposition: Lemma shell_not_empty' : exists sb : seq B, exists Hsb : size sb == n, Tuple Hsb \in V.-shell ta.
proof: Proof. exists (flatten (map (fun a => flatten (map (fun b => nseq (JType.f V a b) b) (enum B))) (enum A))). set cdom := flatten _. have /eqP Hy : size cdom = n. rewrite size_flatten /shape -map_comp sumn_big_addn big_map [LHS]big_filter. rewrite -[RHS](sum_num_occ_all ta). rewrite [RHS](reindex_onto enum_rank enum_val) => [|i _] ; last by rewrite enum_valK. apply eq_big. - move=> ? /=; by rewrite enum_rankK eqxx. - move=> a _ /=. rewrite [in RHS]enum_rankK. rewrite size_flatten /shape -map_comp sumn_big_addn big_map big_filter. transitivity (\sum_(b : B) JType.f V a b). apply eq_bigr => ? _ /=; by rewrite size_nseq. by rewrite (Hrow_num_occ Hta). exists Hy. rewrite in_set. apply/forallP => a. apply/forallP => b. rewrite /num_co_occ /num_occ /=. apply/eqP. rewrite (@sorted_is_flattened _ _ (@le_rank_trans _) (@le_rank_asym _) (@le_rank_refl _) #|A| (enum A) ta) //; last 4 first. by rewrite cardE. by apply enum_uniq. by apply sorted_enum. move=> ? _; by rewrite mem_enum. have -> : [seq filter (pred1 elt) ta | elt <- enum A] = [seq nseq N(x0 | ta) x0 | x0 <- enum A]. apply eq_in_map => ? _; by rewrite filter_pred1_num_occ. have sz_flat : forall a, size (flatten [seq nseq (JType.f V a b) b | b <- enum B]) = N(a | ta). move=> a'; rewrite size_flatten /shape -map_comp sumn_big_addn big_map. rewrite -(Hrow_num_occ Hta a') /= enumT. apply eq_bigr => b' _; by rewrite size_nseq. set dom := flatten _. have Hdom : size dom = n. rewrite /dom size_flatten /shape -map_comp sumn_big_addn big_map. rewrite big_filter -[RHS](sum_num_occ_alt ta). apply eq_bigr => a' _ /=; by rewrite size_nseq. move/eqP in Hy. rewrite -size_filter (_ : filter _ _ = filter (predI (fun x => x.2 == b) (fun x => x.1 == a)) (zip dom cdom)); last first. apply eq_in_filter; case=> i1 i2 Hi /=; by rewrite xpair_eqE andbC. rewrite filter_predI (@filter_zip_L _ _ n) //. have -> : mask (map (pred1 a) dom) cdom = flatten [seq nseq (JType.f V a b) b | b <- enum B]. have [A1 [A2 A12]] : exists A1 A2, enum A = A1 ++ a :: A2. have /splitPr[A1 A2] : a \in enum A by rewrite mem_enum. by exists A1, A2. rewrite /cdom /dom A12 map_cat flatten_cat map_cat. rewrite [in X in mask _ X]map_cat flatten_cat mask_cat; last first. rewrite size_map size_flatten /shape -map_comp sumn_big_addn big_map. rewrite size_flatten /shape -map_comp sumn_big_addn big_map. apply eq_bigr => i _ /=; by rewrite sz_flat size_nseq. rewrite (_ : _ :: _ = [:: a] ++ A2) //. rewrite map_cat. rewrite [in X in _ ++ mask _ X = _]map_cat flatten_cat. rewrite mask_cat; last first. by rewrite size_map /= cats0 sz_flat size_nseq. transitivity (mask (map (pred1 a) (flatten [seq nseq N(a1 | ta) a1 | a1 <- [:: a]])) (flatten [seq flatten [seq nseq (JType.f V a1 b1) b1 | b1 <- enum B] | a1 <- [:: a]])). move: (enum_uniq A); rewrite A12 cat_uniq /= negb_or /=. case/andP => uniqA1 /andP [] /andP [a_A1 _] /andP [a_A2 _]. rewrite {1}(_ : mask _ _ = [::]); last by rewrite map_pred1_nseq // mask_false. rewrite (_ : mask (map _ (flatten [seq _ a | a <- A2])) _ = [::]); last first. by rewrite map_pred1_nseq // mask_false. by rewrite 3!cats0 cat0s. rewrite /= 2!cats0 map_nseq /= eqxx mask_true // sz_flat; by apply eq_leq. rewrite (@filter_zip_R _ _ N(a | ta)) //; last first. rewrite /dom filter_flatten size_flatten /shape -!map_comp sumn_big_addn. rewrite big_map (bigD1 a) // big1 /= => [|a1 Ha1]. - rewrite (_ : filter _ _ = filter (xpredT) (nseq N(a | ta) a)); last first. apply eq_in_filter => i /nseqP[-> _]; by rewrite /pred1 /= eqxx. by rewrite addn0 filter_predT size_nseq. - rewrite (_ : filter _ _ = filter (xpred0) (nseq N(a1 | ta) a1)); last first. apply eq_in_filter => j /nseqP[-> _]. by rewrite /pred1 /= (negbTE Ha1). by rewrite filter_pred0. rewrite size_zip size_mask; last first. rewrite size_map /dom sz_flat (_ : filter _ _ = nseq N(a | ta) a); last first. by rewrite filter_flatten map_filter_pred1_nseq // ?enum_uniq // ?mem_enum. by rewrite size_nseq. rewrite size_filter. set x1 := count _ _. set x2 := count _ _. have -> : x1 = x2 by rewrite /x1 /x2 count_map; apply eq_in_count. have -> : x2 = JType.f V a b. rewrite /x2 -size_filter (_ : filter _ _ = nseq (JType.f V a b) b); last first. by rewrite filter_flatten map_filter_pred1_nseq // ?enum_uniq // ?mem_enum. by rewrite size_nseq. by apply/minn_idPl. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup perm) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist entropy num_occ channel types