proposition: Lemma comb_V_support d (f : {ffun 'I_m -> 'rV_n}) n0 n1 (s : {set 'I_m}) : d.-support f \subset s -> ~~ [exists m0, (m0 \in s) && (n1 \in 'V(m0, n0))] -> (comb_V d n0 f) ``_ n1 = d ``_ n1.
proof: Proof. move=> H0 H1. rewrite /comb_V /comb; unlock; rewrite mxE. case: pickP => // m1 Hm1. case/boolP : (m1 \in s) => m1s. move: H1; rewrite negb_exists => /forallP/(_ m1). rewrite m1s /=. by case/setD1P : Hm1 => _ ->. by move/supportP : H0 => /(_ _ m1s) => ->. 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