proposition: Lemma beta_inva n0 m0 (d d' : 'rV_n) : n0 \in 'V m0 -> d ``_ n0 = d' ``_ n0 -> beta n0 m0 d = beta n0 m0 d'.
proof: Proof. move=> n0m0 dd'. rewrite /beta dd'. congr (_ * _)%R. apply eq_bigr => m1 Hm1. by apply beta_inva_helper with m0. 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