proposition: Lemma big_cat_tuple_seq {C : finType} m n (F : seq C -> R) : (\sum_(i in {:m.-tuple C} ) \sum_(j in {: n.-tuple C}) (F (i ++ j)) = \sum_(p in {: (m + n)%nat.-tuple C}) (F p))%R.
proof: Proof. move: (@big_cat_tuple _ m n (fun l => if size l == (m + n)%nat then F l else R0)). set lhs := (\sum_(i in _) _)%R => H. apply trans_eq with lhs. apply eq_bigr => /= t _; apply eq_bigr => /= t' _. case: ifP => //; by rewrite size_tuple eqxx. rewrite H; apply eq_bigr => /= t _; by rewrite size_tuple eqxx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix perm) Reals Lra Classical mathcomp(Rstruct classical_sets) ssrZ ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy aep typ_seq joint_typ_seq channel channel_code