proposition: Lemma dprojs_V2_pfamily d m0 n0 (m0n0 : n0 \in 'V m0) t d' (d'td : dproj d' ('V m0 :\ n0) t = d) (d't : freeon (`V(m0, n0) :\ n0) d' t) : dprojs_V2 H d m0 n0 t \in pfamily d ('V m0 :\ n0) (fun n1 => [pred t0 | (dprojs_V H d n1 t0 \in pfamily d (`F n1 :\ m0) (fun m1 => freeon (`V(m1, n1) :\ n1) d)) && (comb_V H d n1 (dprojs_V H d n1 t0) == t0)]).
proof: Proof. pose pT : predType _ := [predType of simpl_pred 'rV['F_2]_n]. apply/(@pfamilyP _ _ pT); split. apply/supportP => n1. rewrite 2!inE /= negb_and negbK. case/orP => [ /eqP ->{n1}| m0n1]. apply/rowP => n2 /=. by rewrite /dprojs_V2 dprojs_out // inE /ssgraph 2!inE eqxx. apply/rowP => n2 /=. by rewrite /dprojs_V2 dprojs_out // inE /ssgraph in_setD1 (negbTE m0n1) andbF. move=> /= n1 Hn1. rewrite {1}/in_mem /=. apply/andP; split. apply/familyP => /= m1. rewrite {1}/in_mem /=. rewrite inE /= in_set1 /=. case: ifPn. case/andP => m1m0 m1n1. apply/forallP => n2. apply/implyP => Hn2. by rewrite /dprojs_V2 dprojs_out. rewrite negb_and negbK. case/orP => [ | m1n1 /=]. move/eqP => -> {m1} /=. rewrite /dprojs_V /dprojs_V2. apply/eqP/rowP => n2. case/boolP : (n2 \in `V( m0, n1) :\ n1) => K; last by rewrite dprojs_out. rewrite dprojs_in //. case/boolP : (n2 \in ssgraph H m0 n0 n1) => L; last first. by rewrite dprojs_out. rewrite dprojs_in //. move: L; rewrite inE => /andP[L]. case/existsP => m1 /andP[Hm1 n2m1n1]. rewrite -d'td. case/boolP : (n2 \in 'V m0 :\ n0) => n2m0n0; first by rewrite dproj_in. rewrite dproj_out // (freeon_notin d't) //. rewrite in_setD1 negb_and negbK. rewrite /= in_setD1 negb_and negbK in n2m0n0. case/orP : n2m0n0 => [->// | n2m0]. suff : n2 \notin `V(m0, n0) by move => ->; rewrite orbC. apply/negP. by apply: disjoint_Vgraph2 n2m1n1 n2m0. apply/eqP/rowP => n2. rewrite dprojs_out //. apply/negP. rewrite /= in_setD1. case/andP => Hn2' Hn2. move/negP : Hn2'; apply. rewrite Vgraph_set1 in Hn2. by rewrite in_set1 in Hn2. by rewrite -FnextE. rewrite comb_dprojs_V //. case/boolP: [exists m1, (m1 \in `F n1 :\ m0) && (n1 \in `V( m1, n1))] => X. rewrite /dprojs_V2 dprojs_in //; last by rewrite inE /ssgraph Hn1 X. by rewrite -d'td dproj_in. by rewrite /dprojs_V2 dprojs_out // inE /ssgraph 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