proposition: Lemma checksubsum_dproj d t s s0 : (forall i, i \in s :\: s0 -> t ``_ i = d ``_ i) -> \delta s (dproj d s0 t) = \delta s t.
proof: Proof. move=> H1. rewrite /checksubsum; congr (_ == Zp0). apply eq_big => n1 // Hn1. case/boolP : (n1 \in s0) => [H|H]; first by rewrite dproj_in. by rewrite dproj_out // H1 // in_setD H. 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