proposition: Lemma dprojs_V2_in d m0 n0 t n1 (Hn1 : n1 \in 'V m0 :\ n0) (Ht : comb_V2 H d m0 n0 (dprojs_V2 H d m0 n0 t) = t) : ((dprojs_V2 H d m0 n0 t) n1) ``_ n1 = t ``_ n1.
proof: Proof. case/boolP : [exists m1, (m1 \in `F n1 :\ m0)] => [/existsP[m1 K]|K]. rewrite /dprojs_V2 dprojs_in // inE /ssgraph Hn1 /=. by apply/existsP; exists m1; rewrite K root_in_Vgraph. rewrite dprojs_out /=; last first. rewrite inE /ssgraph Hn1 /=. apply: contra K => /existsP[x /andP[Hx _]]. by apply/existsP; exists x. rewrite -Ht. rewrite /comb_V2 /dprojs_V2 /= /comb; unlock; rewrite mxE. case: pickP => // n3. rewrite inE => /andP[Hn3 /existsP[m1 /andP[Hm1 Hn1'']]]. rewrite negb_exists in K. suff n31 : n3 = n1. move/forallP : K => /(_ m1). by rewrite -{1}n31 Hm1. move: Hn1''. rewrite inE in_set1 /= => /orP[/eqP //|]. rewrite 2!inE. case/andP => m1n3 /connectP [] /= p. case/shortenP => p' Hp' Hun pp' Hlast. exfalso. apply (@Hacyclic [:: inl m0, inr n3, inl m1 & p'] isT). apply: uniq_path_ucycle_extend_1 => //. - by rewrite /= -VnextE; move: Hn3; rewrite in_setD1 => /andP[]. - rewrite rcons_path Hp' /= -Hlast exceptE /= andbT -VnextE. move: Hn1; rewrite in_setD1 => /andP[_ -> /=]. rewrite eq_sym (path_except_neq _ Hp') // Hlast. destruct p' => //=; by rewrite mem_last. - rewrite rcons_uniq Hun andbT inE negb_or. apply/andP; split. apply/eqP; case => ?; subst m1. by rewrite in_setD1 eqxx in Hm1. apply/negP => Hx. case/splitPr : Hx => p1 p2 in Hp' Hun pp' Hlast. rewrite last_cat /= in Hlast. apply (@Hacyclic [:: inl m0, inr n3, inl m1 & p1] isT). apply: uniq_path_ucycle_extend_1 => //. + by rewrite /= -VnextE; move: Hn3; rewrite in_setD1 => /andP[]. + by move: Hp'; rewrite -cat_rcons cat_path => /andP[]. + rewrite rcons_uniq. move: Hun; rewrite -cat_cons cat_uniq => /andP[-> /=]. by rewrite negb_or -andbA => /andP[ ->]. 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