proposition: Lemma perm_tuple_in_Ttuples ta (s : 'S_n) : perm_tuple s ta \in T_{P} <-> ta \in T_{P}.
proof: Proof. rewrite 2!in_set. split => /forallP H; apply/forallP => a; move: H => /(_ a)/eqP => ->; by rewrite num_occ_perm. 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