proposition: Lemma sub_vec_dproj d t s' s : s \subset s' -> (dproj d s' t) \# s = t \# s.
proof: Proof. move=> s's. rewrite /dproj; unlock; apply/rowP => i; rewrite !mxE; case: ifPn => //. move/subsetP: s's => /(_ (enum_val i)); by rewrite enum_valP => ->. 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