proposition: Lemma sub_vec_dprojs d t A (g : A -> {set 'I_n}) s a : s \subset g a -> ((dprojs d g t) a) \# s = t \# s.
proof: Proof. rewrite /dprojs; unlock => H0; by rewrite ffunE sub_vec_dproj. 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