proposition: Lemma size_seqs_but1 (l1 l2 : seq R2) : size (seqs_but1 l1 l2) = size l2.
proof: Proof. elim: l2 => [|x l2 IH] //= in l1 *. by rewrite IH. 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