proposition: Lemma alpha_two_successors n1 n2 m1 d : n1 != n2 -> 'V m1 = [set n1; n2] -> alpha m1 n1 d = beta n2 m1 (d `[ n2 := d ``_ n1 ]).
proof: Proof. move=> n1n2 Hm1. rewrite recursive_computation; last by rewrite Hm1 in_setU in_set1 eqxx. rewrite Hm1 (_ : [set n1; n2] :\ n1 = [set n2]); last by rewrite setU1K // in_set1. rewrite rsum_freeon1 2!big_set1. do 2 rewrite checksubsum_set2 //. rewrite [in X in X%:R]/row_set !mxE (negbTE n1n2) eqxx. case/boolP : (d ``_ n1 == Zp0). move/eqP => dn1. by rewrite dn1 mul1R /= mul0R addR0. rewrite mul0R add0R -F2_eq1 => /eqP ->. by rewrite eqxx mul1R. 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