proposition: Lemma sub_vec_dprojs_V2 d m0 n0 t n1 m1 : n1 \in 'V m0 :\ n0 -> m1 \in `F n1 :\ m0 -> (dprojs_V2 d m0 n0 t) n1 \# `V(m1, n1) :\ n1 = t \# `V(m1, n1) :\ n1.
proof: Proof. move=> Hn1 Hm1; rewrite /dprojs_V2 sub_vec_dprojs //. apply/subsetP => n2 Hn2. rewrite inE /ssgraph Hn1 /=; apply/existsP; exists m1; rewrite Hm1. by move: Hn2; rewrite in_setD1 => /andP[]. 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