proposition: Lemma big_cat_tuple {C : finType} m n (F : (m + n)%nat.-tuple C -> R) : (\sum_(i in {:m.-tuple C}) \sum_(j in {: n.-tuple C}) F [tuple of (i ++ j)] = \sum_(p in {: (m + n)%nat.-tuple C}) (F p))%R.
proof: Proof. elim: m n F => [m2 F /=|m IH n F]. - transitivity (\sum_(i <- [tuple] :: [::]) \sum_(j in {: m2.-tuple C}) F [tuple of i ++ j] )%R. apply congr_big => //=. apply (@eq_from_nth _ [tuple]); rewrite /index_enum -enumT /= (eqP (enum_tupleP _)) card_tuple expn0 //. move=> i; rewrite ltnS leqn0 => /eqP ->. rewrite tupleE /=. case: (enum _) => //= t. by rewrite (tuple0 t). rewrite big_cons /= big_nil /= addR0. apply eq_bigr => // i _; congr F. exact/val_inj. - symmetry. transitivity (\sum_(p in tuple_finType (m + n).+1 C) F p)%R; first by apply congr_big. rewrite -(@big_tuple_cons_behead _ _ _ xpredT xpredT). rewrite -(@big_tuple_cons_behead _ _ _ xpredT xpredT). apply eq_bigr => i _. move: {IH}(IH n (fun x => F [tuple of i :: x])) => <-. apply eq_bigr => /= t _; apply eq_bigr => /= t' _; congr F. exact/val_inj. 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