proposition: Lemma typed_tuples_not_empty' : exists x : seq A, exists Hx : size x == n, Tuple Hx \in T_{P}.
proof: Proof. exists (flatten (map (fun x0 => nseq (type.f P x0) x0) (enum A))). have Hx : size (flatten [seq nseq (type.f P x0) x0 | x0 <- enum A]) == n. rewrite size_flatten /shape -map_comp sumn_big_addn big_map. case: (P) => P' f HP' /=. apply/eqP. transitivity (\sum_(a in A) f a)%nat; last first. apply/eqP; by apply ffun_of_fdist with P'. apply congr_big => //. by rewrite enumT. move=> a /= _. by rewrite size_nseq. exists Hx. rewrite inE. apply/forallP => a. rewrite /num_occ /= -size_filter. rewrite filter_flatten size_flatten /shape -!map_comp sumn_big_addn big_map. rewrite (bigD1 a) // big1 /= => [|a' Ha']. - rewrite addn0 -(INR_type_fun P). apply/eqP. do 2 f_equal. rewrite -{1}(_ : size (nseq (type.f P a) a) = type.f P a); last by rewrite size_nseq. congr (size _). apply/esym/all_filterP/all_pred1P. by rewrite size_nseq. - transitivity (size (@List.nil A)) => //. congr (size _). apply/eqP/negPn; rewrite -has_filter; apply/hasPn => l Hl. by case/nseqP : Hl => ->. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum perm) mathcomp(matrix) mathcomp(Rstruct) Reals ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist proba entropy num_occ channel_code channel typ_seq