proposition: Lemma checksubsum_dprojs_V2 d m0 n0 (t' t : 'rV_n) n1 m1 m2 (Hn1 : n1 \in 'V m0 :\ n0) (Hm1 : m1 \in `F n1 :\ m0) (Hm2 : m2 \in `F(m1, n1)) : dprojs_V2 d m0 n0 t \in pfamily t' ('V m0 :\ n0) (fun n2 => [pred t'' | (dprojs_V H d n2 t'' \in pfamily d (`F n2 :\ m0) (fun m2 => freeon (`V(m2, n2) :\ n2) d)) && (comb_V H d n2 (dprojs_V H d n2 t'') == t'')]) -> \delta ('V m2) ((dprojs_V H d n1 ((dprojs_V2 d m0 n0 t) n1)) m1) = \delta ('V m2) t.
proof: Proof. move=> H0; rewrite /checksubsum; congr (_ == _). apply eq_bigr => n2 n2m2. rewrite /dprojs_V /dprojs_V2. case/boolP : (n2 \in `V( m1, n1) :\ n1) => [Hn2|]. rewrite dprojs_in // dprojs_in //inE /ssgraph Hn1 /=. apply/existsP; exists m1; rewrite Hm1. by case/setD1P : Hn2. move=> Hn2; rewrite dprojs_out //; move: Hn2. rewrite in_setD1 negb_and negbK. case/boolP : (n2 == n1) => [/eqP ?|/=]; last first. by move/(Fgraph_Vnext_Vgraph Hm2 n2m2) => ->. subst n2 => /=. pose pT : predType _ := [predType of simpl_pred 'rV['F_2]_n]. case/(@pfamilyP _ _ pT): H0 => H0 /(_ _ Hn1). rewrite inE => /andP[_]. move/eqP/rowP/(_ n1). rewrite comb_dprojs_V_not_in_partition; last first. by move=> m3; rewrite in_setD1 eqxx. rewrite /dprojs_V2 dprojs_in // inE Hn1 /=. apply/existsP; exists m1; by rewrite Hm1 /= root_in_Vgraph. 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