proposition: Lemma checksubsum_dproj_freeon d s0 s t : freeon s0 d t -> \delta s (dproj d s0 t) = \delta s t.
proof: Proof. move=> Ht. rewrite checksubsum_dproj // => i; rewrite in_setD => /andP[H1 H2]. by rewrite (freeon_notin Ht). 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