proposition: Lemma pfamily_dprojs_V d n0 t : dprojs d (sgraph n0) t \in pfamily d ('F n0) (fun m0 => [pred t | freeon (sgraph n0 m0) d t]).
proof: Proof. pose pT : predType _ := [predType of simpl_pred 'rV['F_2]_n]. apply/(@pfamilyP _ _ pT); split. apply/supportP => m0 n0m0. apply/rowP => n1. rewrite dprojs_out //. apply: contra n0m0. rewrite FnextE; exact: mem_VgraphD1_Vnext. move=> m0 m0n0; by rewrite inE (freeon_dprojs _ _ (sgraph n0)). 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