proposition: Lemma big_tuple_cons_behead {C : finType} n (F : n.+1.-tuple C -> R) (P1 : pred C) (P2 : pred {: n.-tuple C}) : \sum_(i in C | P1 i) \sum_(j in {: n.-tuple C} | P2 j) (F [tuple of (i :: j)]) = \sum_(p in {: n.+1.-tuple C} | (P1 (thead p)) && (P2 (tbehead p)) ) (F p).
proof: Proof. apply/esym. rewrite (partition_big (fun x => thead x) (fun x => P1 x)) //=; last first. move=> t; by case/andP. apply eq_bigr => i Hi. rewrite (reindex_onto (fun j : {: n.-tuple C} => [tuple of (i :: j)]) (fun p => [tuple of (behead p)])) /=; last first. move=> j /andP[Hj1 /eqP <-]; exact/esym/tuple_eta. apply congr_big => // x /=. rewrite !theadE eqxx /= Hi /= -andbA /=. rewrite (_ : _ == x = true) ?andbT; last first. rewrite tupleE /behead_tuple /=; exact/eqP/val_inj. congr P2; rewrite /tbehead tupleE /behead_tuple; 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