proposition: Lemma dproj_prop d m0 n0 d' t (d'd : freeon ('V m0 :\ n0) d' d) (Hpfamily : 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)])) (Ht : comb_V2 H d m0 n0 (dprojs_V2 H d m0 n0 t) = t) : dproj d' ('V m0 :\ n0) t == d.
proof: Proof. apply/eqP/rowP => n1. case/boolP : (n1 \in 'V m0 :\ n0) => K; last first. by rewrite dproj_out // (freeon_notin d'd). rewrite dproj_in //. move: K. rewrite /= in_setD1. case/andP => n1n0 Hn1. pose pT : predType _ := [predType of simpl_pred 'rV['F_2]_n]. case/(@pfamilyP _ _ pT): Hpfamily => _ /(_ n1). rewrite inE in_set1 n1n0 /= => /(_ Hn1). rewrite {1}/in_mem /=. case/andP => /pfamilyP[Hlhs11 Hlhs12]. rewrite /comb_V /dprojs_V /dprojs_V2. move/eqP/(congr1 (fun x : 'rV_n => x ``_ n1)). rewrite /comb; unlock => /=. rewrite mxE. case: pickP => [m1 Hm1 | _]. by rewrite in_setD1 eqxx in Hm1. case/boolP : (n1 \in ssgraph H m0 n0 n1) => [L|L]. by rewrite dprojs_in. rewrite dprojs_out //. move: L. rewrite /ssgraph inE negb_and in_setD1 Hn1 andbT negbK (negbTE n1n0) orFb. move=> tmp _. rewrite -{}Ht comb_dprojs_V2_Vnext_dangling //. apply: contra tmp => /existsP[m1 Hm1]. apply/existsP; exists m1; rewrite Hm1 /=; exact: 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