proposition: Lemma cond_type_equiv : row_num_occ P V <-> [forall ta, (ta \in T_{P}) ==> (V.-shell ta != set0)].
proof: Proof. split=> H. - apply/forallP => ta. apply/implyP => Hta. apply/set0Pn. by apply shell_not_empty with P. - move=> ta Hta a. move/forallP : H => /(_ ta)/implyP/(_ Hta). case/set0Pn => tb. rewrite /shell in_set. move/forallP/(_ a)/forallP => H. rewrite -(num_co_occ_num_occ ta tb). apply eq_bigr => b _. by move/eqP : (H b) => <-. 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