proposition: Lemma dprojs_comb_V d n0 (g : 'I_n -> {set 'I_m}) (f : {ffun 'I_m -> 'rV_n}) : f \in pfamily d (g n0) (fun i => freeon ('V(i, n0) :\ n0) d) -> dprojs_V H d n0 (comb_V H d n0 f) = f.
proof: Proof. rewrite inE /= => /forallP => /= Hf. apply/ffunP => /= m0. apply/rowP => n1. case/boolP : (n1 \in 'V( m0, n0) :\ n0) => Hn1. rewrite dprojs_in //. by rewrite (@comb_V_in _ _ _ m0) //. rewrite dprojs_out //. move: (Hf m0). case: ifP => [_ | _ /eqP -> //]. rewrite inE. by move/freeon_notin => ->. 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