proposition: Lemma another_Fgraph_injective (m0 : 'I_m) (n0 n1 n2 : 'I_n) (Hn1 : n1 \in 'V m0 :\ n0) (Hn2 : n2 \in 'V m0 :\ n0) : 'F n1 :\ m0 != set0 -> \bigcup_(m1 in 'F n1 :\ m0) 'F(m1, n1) = \bigcup_(m1 in 'F n2 :\ m0) 'F(m1, n2) -> n1 = n2.
proof: Proof. move=> Hset0. move=> abs. apply/eqP/negPn/negP => n1n2. have {}Hset0 : \bigcup_(m1 in 'F n1 :\ m0) 'F(m1, n1) != set0. apply: contra Hset0; exact: bigcup_succ_set0. case/set0Pn : Hset0 => /= m1 Habs. move: (Habs). case/bigcupP => /= m2 Hm2 Hm1. rewrite !inE /= in Hm1. case/andP : Hm1 => m2n1. case/connectP => /= p. case/shortenP => p' Hp' unp pp' lastp. rewrite abs in Habs. move: Habs. case/bigcupP => /= m3 Hm3 Hm1'. rewrite !inE /= in Hm1'. case/andP : Hm1' => m3n2. case/connectP => /= p0. case/shortenP => p0' Hp0' unp0 p0p0' lastp0. destruct p' as [|p'1 p'2]. rewrite /= in lastp. case: lastp => ?; subst m2. suff : ucycle (tanner_rel H) (inr n1 :: inl m0 :: inr n2 :: inl m3 :: p0'). exact: Hacyclic. apply: uniq_path_ucycle_extend_2. exact: sym_tanner_rel. exact: simple_tanner_rel. by []. by rewrite /= -VnextE; move: Hn2; rewrite in_setD1 => /andP[]. by []. by rewrite /= -VnextE; move: Hn1; rewrite in_setD1 => /andP[]. apply/eqP; case => ?; subst m3; by rewrite in_setD1 eqxx in Hm3. rewrite rcons_path Hp0' /= exceptE /= -lastp0 /= sym_tanner_rel m2n1 /=. by apply: contra n1n2 => /eqP [] ->. by []. destruct p0' as [|p0'1 p0'2]. rewrite /= in lastp0. case: lastp0 => ?; subst m3. suff : ucycle (tanner_rel H) (inr n2 :: inl m0 :: inr n1 :: inl m2 :: p'1 :: p'2). exact: Hacyclic. apply: uniq_path_ucycle_extend_3. exact: sym_tanner_rel. exact: simple_tanner_rel. by []. by move: Hp' => /= /andP[] /except_rel. by move: Hp' => /= /andP[] /except_rel. by rewrite /= -VnextE; move: Hn1; rewrite in_setD1 => /andP[]. by rewrite /= -VnextE; move: Hn2; rewrite in_setD1 => /andP[]. apply/eqP; case => ?; subst m2; by rewrite in_setD1 eqxx in Hm2. move/path_except_notin : Hp'; rewrite inE negb_or => /andP []; by rewrite eq_sym. by apply: contra n1n2 => /eqP [] ->. rewrite rcons_path; apply/andP; split. rewrite /= in Hp'. case/andP : (Hp') => Hp'1 Hp'2. apply: sub_path_except Hp'2. apply/eqP => ?; subst p'1. by move/andP : Hp'; rewrite exceptE /= {1}tanner_relE; case. apply/negP => m2p'2. move: unp. rewrite -(cat1s (inl m2)) -(cat1s p'1) uniq_catCA uniq_catC cat_uniq. case/andP => /andP []; by rewrite m2p'2. rewrite /= in lastp. rewrite /= exceptE /= andbT -lastp /= sym_tanner_rel m3n2 /=. apply/eqP; case => ?; subst m2. move: unp. by rewrite cons_uniq lastI mem_rcons inE -lastp /= eqxx. rewrite [p'1 :: _]lock /= -lock in unp; by case/andP : unp. suff : ucycle (tanner_rel H) ((inl m1 :: rev (belast p0'1 p0'2)) ++ (inl m3 :: inr n2 :: inl m0 :: inr n1 :: inl m2 :: belast p'1 p'2)). apply Hacyclic; by rewrite size_cat addnC. apply: uniq_path_ucycle_cat_extend; try assumption. exact: sym_tanner_rel. exact: simple_tanner_rel. by rewrite /= -VnextE; move: Hn2; rewrite in_setD1 => /andP[]. by rewrite /= -VnextE; move: Hn1; rewrite in_setD1 => /andP[]. apply/eqP; case => ?; subst m3; by rewrite in_setD1 eqxx in Hm3. apply/eqP; case => ?; subst m2; by rewrite in_setD1 eqxx in Hm2. by rewrite lastp last_cons -lastI. by rewrite lastp0 last_cons -lastI. move: unp. rewrite (cons_uniq (inl m2)) => /andP [] H1 H2. rewrite cons_uniq. apply/andP; split. apply: contra H1; by move/mem_belast. rewrite lastI rcons_uniq in H2; by case/andP : H2. move: unp0. rewrite (cons_uniq (inl m3)) => /andP [] H1 H2. rewrite cons_uniq. apply/andP; split. apply: contra H1; by move/mem_belast. rewrite lastI rcons_uniq in H2; by case/andP : H2. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2