proposition: Lemma dprojs_in d t A (g : A -> {set 'I_n}) n0 a : n0 \in g a -> ((dprojs d g t) a) ``_ n0 = t ``_ n0.
proof: Proof. move=> ?; by rewrite /dprojs; unlock; rewrite ffunE dproj_in. 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