proposition: Lemma disjoint_Vgraph2 m0 n0 n1 n2 m1 (m0n0 : n0 \in 'V m0) : n1 \in 'V m0 :\ n0 -> n2 \in 'V(m0, n1) :\ n1 -> m1 \in 'F n1 :\ m0 -> n2 \in 'V(m1, n1) -> n2 \notin 'V m0 -> n2 \in 'V(m0, n0) -> Logic.False.
proof: Proof. move=> Hn1 Hn2 Hm1 H1 H2 H3. move: (trivIset_Vgraph_part_vnode n1). move/trivIsetP. move/(_ ('V(m0, n1) :\ n1) ('V(m1,n1) :\ n1)). rewrite /Vgraph_part_vnode. have K1 : 'V(m0, n1) :\ n1 \in [set 'V(m2, n1) :\ n1 | m2 in 'F n1]. apply/imsetP. exists m0 => //. by move: Hn1; rewrite in_setD1 -FnextE => /andP[]. move/(_ K1). have K2 : 'V(m1, n1) :\ n1 \in [set 'V(m2, n1) :\ n1 | m2 in 'F n1]. apply/imsetP. exists m1 => //. rewrite inE in Hm1. by case/andP : Hm1. move/(_ K2). have K3 : 'V(m0, n1) :\ n1 != 'V(m1, n1) :\ n1. have K4 : n0 \in 'V(m0, n1) :\ n1. rewrite !inE. rewrite !inE in Hn1. case/andP : Hn1 => n1n0 m0n1. rewrite eq_sym n1n0 /= -VnextE (negbTE n1n0) /= m0n1 /=. apply/connect1. rewrite exceptE /= -VnextE m0n0 /=. by apply: contra n1n0 => /eqP[->]. have K5 : n0 \notin 'V(m1, n1) :\ n1. rewrite !inE negb_and negbK negb_or /=. rewrite !inE in Hn1. case/andP : Hn1 => n1n0 m0n1. rewrite eq_sym (negbTE n1n0) /= negb_and. rewrite !inE in Hm1. apply/orP; right. apply/negP. case/connectP => p. case/shortenP => p' Hp' Hun pp' Hlast. suff : ucycle (tanner_rel H) (inl m0 :: inr n1 :: inl m1 :: p'). exact: Hacyclic. apply: uniq_path_ucycle_extend_1 => //. exact: simple_tanner_rel. by rewrite /= -VnextE; case/andP : Hm1. by rewrite /= -VnextE -FnextE; case/andP : Hm1. rewrite rcons_path Hp' /= exceptE /= andbT -Hlast -VnextE m0n0 /=. apply/eqP; case => ?; subst n1. by rewrite in_setD1 eqxx in K4. rewrite rcons_uniq Hun andbT /= !inE /= negb_or. apply/andP; split. apply/eqP; case => ?; subst m1; by rewrite eqxx in Hm1. apply/negP => m0p. case/splitPr : m0p => p1 p2 in Hp' Hun pp' Hlast. suff : ucycle (tanner_rel H) (inl m0 :: inr n1 :: inl m1 :: p1) by apply Hacyclic. apply: uniq_path_ucycle_extend_1. exact: simple_tanner_rel. by rewrite /= -VnextE. rewrite /= -VnextE -FnextE; by case/andP : Hm1. rewrite -(cat1s (inl m0)) catA cat_path in Hp'. rewrite !cats1 in Hp'. by case/andP : Hp'. rewrite rcons_uniq. move: Hun. rewrite -cat_cons cat_uniq => /andP[->]; rewrite andbT. by rewrite /= negb_or -andbA => /and3P[]. apply/eqP. move/setP/(_ n0). by rewrite K4 (negbTE K5). move/(_ K3)/disjoint_setI0/setP/(_ n2). rewrite inE Hn2 /= in_set0 in_setD1 H1. rewrite in_setD1 in Hn2. case/andP : Hn2. by move=> -> _. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2