proposition: Lemma freeon_dproj d t s : freeon s d (dproj d s t).
proof: Proof. apply/forallP => n1; apply/implyP => n1s; by rewrite dproj_out. 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