proposition: Lemma dproj_in d t s i : i \in s -> (dproj d s t) ``_ i = t ``_i.
proof: Proof. move=> H; by rewrite /dproj; unlock; rewrite mxE H. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg zmodp matrix) Reals mathcomp(Rstruct) ssr_ext ssralg_ext ssrR Reals_ext f2 summary subgraph_partition tanner tanner_partition fdist channel checksum