proposition: Lemma Vgraph_decompose n1 m0 n0 : n0 \in 'V m0 -> n1 \in 'V(m0, n0) -> n1 != n0 -> n1 \notin 'V m0 -> exists n1', n1' \in 'V m0 :\ n0 /\ exists m1, m1 \in 'F n1' :\ m0 /\ n1 \in 'V(m1, n1').
proof: Proof. move=> m0n0 Hn1 n1n0 n1Vm0. rewrite !inE (negbTE n1n0) /= in Hn1. case/andP : Hn1 => _. case/connectP => /= q Hq Hq'. case/shortenP : Hq Hq' => /= p Hp Huniq pq Hp'. destruct p as [|[?|n1'] p]; [by [] | by rewrite exceptE /= tanner_relE in Hp | ]. rewrite /= in Hp'. rewrite /= {1}exceptE /= -andbA in Hp. case/and3P : Hp => m0n1' n1'n0 Hp. have n1n1' : n1 != n1'. apply/eqP => ?; subst n1'. by move: n1Vm0; rewrite VnextE sym_tanner_rel m0n1'. destruct p as [|[m1|?] t]; [ | | by rewrite exceptE /= tanner_relE in Hp ]. exfalso; move/negP : n1n1'; apply. by case: Hp' => ->. move: Hp; rewrite /= {1}exceptE; case/andP => /and3P[/= m1n1' _ _] Hp. exists n1'. rewrite !inE /=. split. rewrite VnextE sym_tanner_rel m0n1' andbT. by apply: contra n1'n0 => /eqP ->. exists m1; split. rewrite in_setD1 FnextE VnextE m1n1' andbT. apply/eqP => ?; subst m1. by rewrite !inE /= eqxx /= in Huniq. rewrite !inE /= (negbTE n1n1') /= m1n1' /=. apply/connectP; exists t => //. apply: (sub_path_except _ _ Hp) => //. case/andP : Huniq => _. rewrite -(cat1s (inr _)) -(cat1s (inl m1)). by rewrite uniq_catCA cat_uniq => /and3P[_ _ /= /andP[]]. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2