proposition: Lemma sum_tuples_ctypes f F : \sum_(tb | F tb) f tb = \sum_(V | V \in \nu^{B}(P)) \sum_ (tb in V.-shell ta | F tb) f tb.
proof: Proof. rewrite big_mkcond /=. transitivity (\sum_(V | V \in \nu^{B}(P)) \sum_(tb in V.-shell ta) if F tb then f tb else 0). exact: sum_tuples_ctypes'. apply eq_bigr => s _. rewrite [in LHS]big_mkcond /= [in RHS]big_mkcond /=. apply/esym/eq_bigr => tb _. by case/boolP : (tb \in s.-shell ta). 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