proposition: Lemma cover_shell : cover shell_partition = [set: n.-tuple B].
proof: Proof. rewrite /cover /cond_type; apply/setP => tb. rewrite in_set; apply/bigcupP. exists (num_co_occ_jtype ta tb).-shell ta. - apply/imsetP; exists (num_co_occ_jtype ta tb) => //. rewrite inE. apply cond_type_equiv => ta' Hta' a. transitivity (\sum_(b in B) N(a, b | ta, tb)). - apply eq_bigr => b _. by rewrite /num_co_occ_jtype /= 2!ffunE. - rewrite num_co_occ_partial_sum_alt. move: Hta'; rewrite in_set => /forallP/(_ a)/eqP => Hta'. move: Hta. rewrite in_set => /forallP/(_ a)/eqP. rewrite Hta' eqR_mul2r; last by apply/invR_neq0; rewrite INR_eq0. by move/INR_eq. - rewrite in_set. apply/forallP => a. apply/forallP => b. by rewrite /num_co_occ_jtype /= 2!ffunE. 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