proposition: Lemma shell_subset_output_type ta : V.-shell ta \subset T_{ `tO( V ) }.
proof: Proof. apply/subsetP => tb; rewrite 2!in_set => Htb. apply/forallP => b. apply/eqP. rewrite /OutType.P /OutType.d /OutType.f ffunE. do 2 f_equal. rewrite -(num_co_occ_partial_sum_alt tb ta). apply eq_bigr => a _. rewrite num_co_occ_sym. by move/forallP/(_ a)/forallP/(_ b)/eqP : Htb. 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