proposition: Lemma Fgraph_injective n0 m0 m1 : n0 \in 'V m0 -> n0 \in 'V m1 -> 'F(m0, n0) = 'F(m1, n0) -> m0 = m1.
proof: Proof. move=> Hm0 Hm1 m0m1. apply/eqP/negPn/negP => abs. have : exists cy, (2 < size cy)%nat /\ ucycleb (tanner_rel H) cy. have : connect (except (tanner_rel H) (inr n0)) (inl m0) (inl m1). have : m0 \in 'F(m1, n0). by rewrite -m0m1 /Fgraph 2!inE connect0 andbT -VnextE. rewrite 2!inE /subgraph. case/andP => n0m1. rewrite connect_sym //; exact/symmetric_except/sym_tanner_rel. case/connectP => /= s H1 H2. case/shortenP : (H1) H2 => /= s' H1' H2' H3' H2. have [/= s1 [s2 s1s2]] : exists s1 s2, s' = s1 ++ inl m1 :: s2. have m1s : inl m1 \in s'. rewrite H2. destruct s' as [|h t]. rewrite /= in H2. case: H2 => ?; subst m1; by rewrite eqxx in abs. by rewrite /= mem_last. case/(nthP (inl m0)) : m1s => i Hi im1. exists (take i s'), (drop i.+1 s'). by rewrite -im1 -drop_nth // cat_take_drop. exists (inr n0 :: inl m0 :: s1 ++ [:: inl m1]). split. by rewrite /= size_cat /= addn1. apply/andP; split; last first. rewrite -/(uniq (inl m0 :: s')) s1s2 -cat1s catA -(cat1s (inl m1)) catA cat_uniq in H2'. case/andP : H2' => H2' H2''. rewrite cons_uniq H2' andbC /= inE /= mem_cat /= negb_or. apply/andP; split => //. apply/negP => abs'. have {}abs' : inr n0 \in s' by rewrite s1s2 mem_cat abs'. case/(nthP (inl m0)) : abs' => i Hi abs'. move/pathP : H1'. move/( _ (inl m0) _ Hi). by rewrite exceptE /= abs' eqxx andbA andbC. rewrite /cycle /=. rewrite -VnextE Hm0 /= rcons_path. apply/andP; split. rewrite s1s2 -cat1s catA cat_path in H1'. case/andP : H1' => H1' _; move: H1'. exact: except_path. by rewrite last_cat /= -VnextE. case=> cy [] H1; exact: Hacyclic. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2