proposition: Lemma Vgraph_id n0 m0 n1 n1' m1 m1' n2 : n0 \in 'V m0 -> n1 \in 'V m0 :\ n0 -> n1' \in 'V m0 :\ n0 -> m1 \in 'F n1 :\ m0 -> m1' \in 'F n1' :\ m0 -> n2 \in 'V(m1, n1) -> n2 \in 'V(m1', n1') -> n1 = n1'.
proof: Proof. move=> Hn0 Hn1 Hn1' Hm1 Hm1'. rewrite !inE. case/orP => [/eqP ? |]; [subst n2|]. case/orP => [/eqP ?|]; [by subst n1'|]. case/andP => n1'm1'. case/connectP => /= p. case/shortenP => p' Hp' unp pp' lastp. exfalso. suff : path.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; move: Hn1'; rewrite in_setD1 => /andP[]. rewrite rcons_path /= Hp' /= exceptE /= -lastp andbT. apply/andP; split. by rewrite /= -VnextE; move: Hn1; rewrite in_setD1 => /andP[]. apply/eqP; case => ?; subst n1'. move/path_except_notin : Hp'. destruct p' => //. rewrite /= in lastp. by rewrite lastI -lastp mem_rcons inE eqxx. rewrite rcons_uniq unp andbT inE negb_or. apply/andP; split. rewrite !inE in Hm1'. case/andP : Hm1' => Hm1' _. by apply: contra Hm1' => /eqP [] ->. apply/negP => Hx. case/splitPr : Hx => p1 p2 in Hp' unp pp' lastp. suff : ucycle (tanner_rel H) [:: inl m0, inr n1', inl m1' & p1]. exact: Hacyclic. apply: uniq_path_ucycle_extend_1 => //. exact: simple_tanner_rel. by rewrite /= -VnextE; move: Hn1'; rewrite in_setD1 => /andP[]. rewrite -(cat1s (inl m0)) catA cat_path in Hp'. rewrite cats1 in Hp'. by case/andP : Hp'. rewrite rcons_uniq. move: unp; rewrite -cat_cons cat_uniq => /andP[-> /=]. by rewrite negb_or -andbA => /and3P[] ->. case/andP => n1m1 /connectP /= [] p. case/shortenP => p' Hp' unp pp' lastp. case/orP => [/eqP ?|]; [subst n1'|]. exfalso. suff : path.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; move: Hn1; rewrite in_setD1 => /andP[]. rewrite rcons_path Hp' /= -lastp exceptE /= andbT -VnextE. rewrite !inE in Hn1'. case/andP : Hn1' => n2n0 -> /=. apply/eqP; case => ?; subst n2. move/path_except_notin : Hp'. destruct p' => //. rewrite /= in lastp. by rewrite lastI mem_rcons -lastp inE eqxx. rewrite rcons_uniq unp 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' unp pp' lastp. suff : ucycle (tanner_rel H) [:: inl m0, inr n1, inl m1 & p1] by exact: Hacyclic. apply: uniq_path_ucycle_extend_1 => //. exact: simple_tanner_rel. by rewrite /= -VnextE; move: Hn1; rewrite in_setD1 => /andP[]. rewrite -(cat1s (inl m0)) catA cat_path in Hp'. rewrite cats1 in Hp'. by case/andP : Hp'. rewrite rcons_uniq. by move: unp; rewrite -cat_cons cat_uniq => /and3P[-> /=]; rewrite negb_or => /andP[->]. move: (Hm1'); rewrite !inE /= -VnextE -FnextE => /andP [] _ -> /=. case/connectP => /= q. case/shortenP => q' Hq' unq qq' lastq. apply/eqP/negPn/negP => n1n1'. case: p' Hp' unp pp' lastp => [// | p'1 p'2] Hp' unp pp' lastp. elim/last_ind : q' Hq' unq qq' lastq => [// | q'1 q'2 _] Hq' unq qq' lastq. rewrite last_rcons in lastq; subst q'2. suff : ucycle (tanner_rel H) ((inr n2 :: rev q'1) ++ [:: inl m1', inr n1', inl m0, inr n1, inl m1 & belast p'1 p'2]). by apply Hacyclic; rewrite size_cat addnC. apply: uniq_path_ucycle_cat_extend => //. exact: sym_tanner_rel. exact: simple_tanner_rel. by rewrite /= -VnextE; move: Hn1'; rewrite in_setD1 => /andP[]. by rewrite /= -VnextE -FnextE; move: Hm1'; rewrite in_setD1 => /andP[]. by rewrite /= -VnextE; move: Hn1; rewrite in_setD1 => /andP[]. apply/eqP; case => ?; subst m1'; by rewrite in_setD1 eqxx in Hm1'. apply/eqP; case => ?; subst m1; by rewrite in_setD1 eqxx in Hm1. by rewrite lastp last_cons -lastI. move: unp. rewrite (lastI p'1) /= mem_rcons inE negb_or => /andP [] /andP [] H1 ->. by rewrite rcons_uniq => /andP []. move: unq. rewrite /= mem_rcons inE negb_or => /andP [] /andP [] -> ->. by rewrite rcons_uniq => /andP [] _ ->. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2