proposition: Lemma beta_def n0 m0 (d : 'rV_n) : let d0 := d `[ n0 := 0 ] in let d1 := d `[ n0 := 1 ] in beta (rW n0) [seq (alpha' m1 n0 d0, alpha' m1 n0 d1) | m1 in 'F n0 :\ m0] = (beta' n0 m0 d0, beta' n0 m0 d1).
proof: Proof. rewrite /rW /beta' /alpha' /ldpc.beta /=. rewrite /image_mem /enum_mem. rewrite -big_filter. rewrite -[in X in _ = (_, X)]big_filter. have [e He [ue Pe perme]] := big_enumP _. rewrite {3 5}/row_set !mxE !eqxx /=. move: (W 0 (vb ``_ n0)) (W 1 (vb ``_ n0)). elim: e {He ue Pe perme} => [|a l IH] p0 p1. by rewrite /= !big_nil !mulR1. by rewrite /= !big_cons /= IH // !mulRA. Qed.
imports: Wf_nat Init.Wf Recdef Reals mathcomp(all_ssreflect perm zmodp matrix ssralg) mathcomp(Rstruct) ssrR Reals_ext ssr_ext ssralg_ext bigop_ext f2 fdist channel pproba linearcode subgraph_partition tanner tanner_partition summary ldpc checksum ldpc_algo