proposition: Lemma comb_V_in d (f : {ffun 'I_m -> 'rV_n}) n0 m0 n1 : n1 \in 'V(m0, n0) :\ n0 -> (comb_V H d n0 f) ``_ n1 = (f m0) ``_ n1.
proof: Proof. move=> Hn1; rewrite /comb_V (@comb_in _ _ _ _ f _ _ m0) //. case: pickP => [m1 Hm1 | ]. case/boolP : (m0 == m1) => [/eqP -> // | m0m1]. have {}Hm1 : n1 \in 'V(m1, n0). move: Hm1; rewrite in_setD1; by case/andP. move: Hn1; rewrite in_setD1; case/andP => n1n0 Hn1. move: (disjoint_Vgraph Hacyclic n1n0 m0m1 Hn1); by rewrite Hm1. move/(_ m0); by rewrite Hn1. 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