proposition: Lemma Vgraph_inclusion n1 m0 n0 m1 n2 : n0 \in 'V m0 -> n1 \in 'V m0 :\ n0 -> m1 \in 'F n1 :\ m0 -> n2 \in 'V(m1, n1) -> n2 \in 'V(m0, n0).
proof: Proof. move=> n0m0 Hn1 Hm1 Hn2. rewrite !inE. case/boolP : (n2 == n0) => //= n2n0. rewrite -VnextE n0m0 /=. rewrite !inE /= in Hn2. case/orP : Hn2 => Hn2. move/eqP in Hn2; subst n2. apply connect1 => /=. move: (Hn1); rewrite in_setD1 exceptE /= -VnextE => /andP[_ -> /=]. by apply: contra n2n0 => /eqP [] ->. case/andP : Hn2 => m1n1 Hn2. case/connectP : Hn2 => p. case/shortenP => p' Hp' Hun p'p Hlast. apply/connectP. exists [:: inr n1, inl m1 & p'] => //. rewrite /=. rewrite !inE /= in Hn1. case/andP : Hn1 => n1n0 Hn1. rewrite {1 2}exceptE /= -VnextE Hn1 /= m1n1 /=. apply/andP; split. by apply: contra n1n0 => /eqP [] ->. apply/andP; split. rewrite andbT. by apply: contra n1n0 => /eqP [] ->. apply (@sub_path_except _ _ (inr n1)) => //. apply/negP => n0p'. case/splitPr : n0p' => p1 p2 in Hp' Hun p'p Hlast. suff : path.ucycle (tanner_rel H) [:: inr n0, inl m0, inr n1, inl m1 & p1]. exact: Hacyclic. apply: uniq_path_ucycle_extend_2 => //. exact: sym_tanner_rel. exact: simple_tanner_rel. by rewrite /= -VnextE. by rewrite /= -VnextE. apply/eqP; case => ?; subst m1; by rewrite in_setD1 eqxx in Hm1. rewrite -(cat1s (inr n0)) catA cats1 cat_path in Hp'; by case/andP : Hp'. rewrite -(cat1s (inl m1)) catA cat_uniq in Hun; by case/andP : Hun. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2