proposition: Lemma Vgraph_injective3 (m0 : 'I_m) (n0 n1 n2 : 'I_n) (Hn1 : n1 \in 'V m0 :\ n0) (Hn2 : n2 \in 'V m0 :\ n0) : n1 |: (\bigcup_(m1 in 'F n1 :\ m0) ('V(m1, n1) :\ n1)) = n2 |: (\bigcup_(m1 in 'F n2 :\ m0) ('V(m1, n2) :\ n2)) -> n1 = n2.
proof: Proof. move=> abs. apply/eqP/negPn/negP => abs'. have [m1] : exists m1, (m1 \in 'F n1 :\ m0) && (n2 \in 'V(m1, n1) :\ n1). move/setP : abs. move/(_ n2) => abs. have {abs} : n2 \in n1 |: \bigcup_(m1 in 'F n1 :\ m0) ('V(m1, n1) :\ n1). by rewrite abs inE in_set1 eqxx. rewrite inE in_set1 eq_sym (negbTE abs') orFb. case/bigcupP => m1 Hm1 n2m1 . exists m1; by rewrite Hm1. case/andP => m1n1. rewrite in_setD1 eq_sym abs' /=. rewrite inE. rewrite in_set1 eq_sym (negbTE abs') /= 2!inE. case/andP => _. case/connectP => p. case/shortenP => p' Hp unp pp' lastp. suff : ucycle (tanner_rel H) [:: inl m0, inr n1, inl m1 & p'] by exact: Hacyclic. apply: uniq_path_ucycle_extend_1. exact: simple_tanner_rel. by rewrite /= -VnextE; move: Hn1; rewrite in_setD1 => /andP[]. by rewrite /= -VnextE -FnextE; move: m1n1; rewrite in_setD1 => /andP[]. rewrite rcons_path Hp /= exceptE /= andbT -lastp. apply/andP; split. by rewrite /= -VnextE; move: Hn2; rewrite in_setD1 => /andP[]. apply/eqP; case=> ?; subst n2; by rewrite eqxx in abs'. rewrite rcons_uniq unp andbT inE negb_or. apply/andP; split. apply/eqP; case => ?; subst m1; by rewrite in_setD1 eqxx in m1n1. apply/negP => m0p'. case/splitPr : m0p' => p'1 p'2 in Hp unp pp' lastp. suff : ucycle (tanner_rel H) [:: inl m0, inr n1, inl m1 & p'1]. exact: Hacyclic. apply: uniq_path_ucycle_extend_1; try assumption. exact: simple_tanner_rel. by rewrite /= -VnextE; move: Hn1; rewrite in_setD1 => /andP[]. by rewrite /= -VnextE -FnextE; move: m1n1; rewrite in_setD1 => /andP[]. rewrite -(cat1s (inl m0)) catA cats1 cat_path in Hp; by case/andP : Hp. rewrite rcons_uniq. by move: unp; rewrite -cat_cons cat_uniq => /and3P[-> /=]; rewrite negb_or => /andP[->]. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2