proposition: Lemma beta_inva_helper n0 m0 m1 (d d' : 'rV_n) : n0 \in 'V m0 -> d ``_ n0 = d' ``_ n0 -> m1 \in 'F n0 :\ m0 -> alpha m1 n0 d = alpha m1 n0 d'.
proof: Proof. move=> n0m0 dd' Hm1. rewrite /alpha. transitivity (\sum_(x = d [~'V(m1, n0) :\ n0]) W ``((y \# 'V(m1, n0) :\ n0) | ((dproj_V m1 n0 d x) \# 'V(m1, n0) :\ n0)) * (\prod_(m2 in 'F(m1, n0)) (\delta ('V m2) (dproj_V m1 n0 d x))%:R))%R. apply eq_bigr => /= t Ht. congr (W ``(_ | _) * _)%R. by rewrite /dproj_V sub_vec_dproj. apply eq_bigr => i Hi. by rewrite checksubsum_dproj_freeon. transitivity (\sum_(x = d [~'V(m1, n0) :\ n0]) W ``((y \# 'V(m1, n0) :\ n0) | ((dproj_V m1 n0 d' x) \# 'V(m1, n0) :\ n0)) * (\prod_(m2 in 'F(m1, n0)) (\delta ('V m2) (dproj_V m1 n0 d' x))%:R))%R. apply eq_bigr => /= i Hi. congr (W ``(_ | _) * _)%R. by rewrite /dproj_V sub_vec_dproj // sub_vec_dproj. apply eq_bigr => j Hj. rewrite /checksubsum. congr ((_ == _)%:R)%R. apply eq_bigr => /= k Hk. rewrite /dproj_V. case/boolP : (k \in 'V( m1, n0) :\ n0) => K. by do 2 rewrite dproj_in //. do 2 rewrite dproj_out //. case/boolP : (k == n0) => [/eqP -> // |kn0]. rewrite in_setD1 kn0 /= in K. exfalso. move/negP : K; apply. move: kn0. by apply Fgraph_Vnext_Vgraph with j. transitivity (\sum_(x = d' [~'V(m1, n0) :\ n0]) W ``((y \# 'V(m1, n0) :\ n0) | ((dproj_V m1 n0 d' x) \# 'V(m1, n0) :\ n0)) * (\prod_(m2 in 'F(m1, n0)) (\delta ('V m2) (dproj_V m1 n0 d' x))%:R))%R; last first. apply/esym. apply eq_bigr => /= t Ht. congr (W ``(_ | _) * _)%R. by rewrite /dproj_V sub_vec_dproj. apply eq_bigr => i Hi. by rewrite checksubsum_dproj_freeon. rewrite (reindex_onto (dproj_V m1 n0 d) (dproj_V m1 n0 d')) /=; last first. move=> ? ?; by rewrite /dproj_V dprojIdef dproj_freeon. apply eq_big => /= i. apply/andP/forallP. case => H1 H2 n1. apply/implyP => Hn1. rewrite in_setD1 negb_and negbK in Hn1. case/orP : Hn1 => Hn1. rewrite (eqP Hn1) -(eqP H2) /dproj_V. have K : n0 \notin 'V( m1, n0) :\ n0 by rewrite in_setD1 eqxx. by rewrite dproj_out. by rewrite -(eqP H2) /dproj_V dproj_out // in_setD1 (negbTE Hn1) andbF. move=> H1. split. apply/forallP => n1; apply/implyP => Hn1. rewrite in_setD1 negb_and negbK in Hn1. case/orP : Hn1 => n1n0. move/eqP : n1n0 => ?; subst n1. by rewrite /dproj_V dproj_out // in_setD1 eqxx. by rewrite /dproj_V dproj_out // in_setD1 (negbTE n1n0) andbC. rewrite /dproj_V dprojIdef dproj_freeon //. by apply/forallP. case/andP=> H1 H2. congr (_ * _)%R. congr (W ``(_ | _)). by rewrite /dproj_V !sub_vec_dproj. apply eq_bigr => m2 Hm2. congr ((_ == _)%:R)%R. apply eq_bigr => n3 Hn3. rewrite /dproj_V. case/boolP : (n3 \in 'V( m1, n0) :\ n0) => K. by rewrite !dproj_in. by rewrite !dproj_out. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix vector ssrnum) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext num_occ bigop_ext fdist channel pproba f2 linearcode subgraph_partition tanner tanner_partition hamming binary_symmetric_channel decoding channel_code summary checksum summary_tanner