proposition: Lemma checksubsum_dprojs_V d n0 t m0 m1 : m1 \in 'F(m0, n0) -> t ``_ n0 = d ``_ n0 -> \delta ('V m1) ((dprojs_V d n0 t) m0) = \delta ('V m1) t.
proof: Proof. move=> Hm1 tn0dn0. rewrite /dprojs_V /dprojs; unlock; rewrite ffunE. rewrite checksubsum_dproj // => n2. rewrite in_setD => /andP[]. rewrite in_setD1 negb_and negbK. case/boolP : (n2 == n0) => [/eqP -> //|/= n2n0 Hn2 Hn2']. move: (Fgraph_Vnext_Vgraph Hm1 Hn2' n2n0). by rewrite (negbTE Hn2). 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