proposition: Corollary msg_nonnil (i1 i2 : id') i {k} t : size (@msg _ _ i1 i2 i k t) > 0 -> i1 \in i ++ labels t /\ i2 \in i ++ labels t.
proof: Proof. move=> Hsz. case Hi1: (i1 \in _). case Hi2: (i2 \in _); first by []. rewrite msg_nil // in Hsz. by rewrite Hi2 orbT. rewrite msg_nil // in Hsz. by rewrite Hi1. 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