proposition: Lemma comb_dprojs_V2_Vnext_dangling d m0 n0 t n1 (n1m0 : n1 \in 'V m0) : ~~ [exists m1, (m1 \in `F n1 :\ m0)] -> (comb_V2 H d m0 n0 (dprojs_V2 H d m0 n0 t)) ``_ n1 = d ``_ n1.
proof: Proof. move=> tmp. rewrite /comb_V2 /dprojs_V2. rewrite /comb; unlock; rewrite mxE. case: pickP => //. move=> n1'; rewrite inE => /andP[Hn1' /existsP[m1' Hm1']]. case/boolP : (n1 \in ssgraph H m0 n0 n1') => [|L]; last first. by rewrite dprojs_out. rewrite dprojs_in; last first. rewrite /ssgraph Hn1' /= inE. apply/existsP; exists m1'; by rewrite Hm1'. rewrite /ssgraph Hn1' /=. case/andP: Hm1' => Hm1'. rewrite 3!inE; case/orP => [/eqP ?|]. subst n1'. move=> abs. rewrite inE in abs. exfalso. move/negP : tmp; apply. case/existsP : abs => m1 /andP[abs _]. apply/existsP; by exists m1. rewrite inE. case/andP => n1'm1' /connectP [] /= p. case/shortenP => p' Hp' Hun p'p Hlast. exfalso. apply (@Hacyclic [:: inl m0, inr n1', inl m1' & p'] isT). apply: uniq_path_ucycle_extend_1 => //. - by rewrite /= -VnextE; move: Hn1'; rewrite in_setD1 => /andP[]. - rewrite rcons_path Hp' /= -Hlast. rewrite exceptE /= andbT -VnextE n1m0 /= eq_sym. rewrite (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 => m0m1'; by move: Hm1'; rewrite m0m1' in_setD1 eqxx. apply/negP => Hx. case/splitPr : Hx => p1 p2 in Hp' Hun p'p Hlast. rewrite last_cat /= in Hlast. apply (@Hacyclic [:: inl m0, inr n1', inl m1' & p1] isT). apply: uniq_path_ucycle_extend_1 => //. + by rewrite /= -VnextE; move: Hn1'; rewrite in_setD1 => /andP[]. + move: Hp'; by rewrite -cat_rcons cat_path => /andP[]. + rewrite rcons_uniq. move: Hun; rewrite -cat_cons cat_uniq => /andP[-> /=]. by rewrite negb_or -andbA => /and3P[->]. 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