proposition: Lemma myrel_ok : myrel =2 tanner_rel H.
proof: Proof. rewrite /myrel tanner_relE /tanner_rel' /= /H /=. move=> [a|a] [b|b] //; rewrite mxE. by destruct (F a b). by destruct (F b a). 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