proposition: Lemma trivIset_subgraph_succ2_D1 (Hg : simple g) m n (mn : g m n) : trivIset (subgraph_succ2_D1 mn).
proof: Proof. apply/trivIsetP => /= v1 v2. rewrite /subgraph_succ2_D1. case/imsetP => n1 Hn1 v1n1. case/imsetP => n2 Hn2 v2n2 v1v2. have n1n2 : n1 != n2 by apply: contra v1v2 => /eqP n1n2; rewrite v1n1 v2n2 n1n2. rewrite -setI_eq0. apply/set0Pn; case=> v. rewrite inE => /andP[]. rewrite v1n1 v2n2 !inE. move: Hn1; rewrite !inE => /andP[n1n Hn1]. move: Hn2; rewrite !inE => /andP[n2n Hn2]. case/orP => [ /eqP ->{v} | vn1]. rewrite (negbTE n1n2) /= => /bigcupP[m'2 Hm'2]. rewrite /subgraph inE => /andP[n2m'2 /connectP[l]]. case/shortenP => l' Hl' Hun l'l Hlast. apply: (@trivIset_sub_ver_suc_suc_helper Hg m n1 n2 m'2 l') => //. by move: Hm'2; rewrite in_setD1 => /andP[]. case/orP => [/eqP vn2 | vn2]. move: vn1; rewrite {}vn2 {v} => /bigcupP[m'1 Hm'1]. rewrite /subgraph inE => /andP[n1m'1 /connectP[l]]. case/shortenP => l' Hl' Hun l'l Hlast. apply: (@trivIset_sub_ver_suc_suc_helper Hg m n2 n1 m'1 l') => //. by move: Hm'1; rewrite in_setD1 => /andP[]. case/bigcupP : vn1 => m'1 Hm'1. rewrite /subgraph inE => /andP[n1m'1 /connectP[l]]. case/shortenP => l' Hl' Hunl l'l Hlast. case/bigcupP : vn2 => m'2 Hm'2. rewrite /subgraph inE => /andP[n2m'2 /connectP[k]]. case/shortenP => k' Hk' Hunk k'k Hkast. suff : ucycle g [:: n1, m, n2, m'2 & k' ++ rev (belast m'1 l')] by apply acyclic_g. apply/andP; split. rewrite /= symmetric_g Hn1 /= Hn2 /= n2m'2 /= rcons_cat cat_path. rewrite (except_path Hk') /= rcons_path; apply/andP; split. rewrite -Hkast {1}Hlast rev_path. apply: sub_path Hl' => w1 w2 /except_rel; by rewrite symmetric_g. rewrite (_ : last _ _ = m'1); first by rewrite symmetric_g. rewrite (last_nth m'1) size_rev size_belast. rewrite (_ : _ :: _ = rev (belast m'1 l' ++ [:: last m'2 k'])); last by rewrite rev_cat. rewrite nth_rev; last by rewrite size_cat /= size_belast addn1. rewrite size_cat addnC addSn add0n subSS size_belast subnn nth_cat size_belast. have -> : 0 < size l'. apply: (@trivIset_subgraph_succ2_D1_helper _ m n1 n2 m'1 m'2 v l' k k') => //. by move: Hm'2; rewrite in_setD1 => /andP[]. by destruct l'. rewrite -(cat1s n1) -(cat1s m) -(cat1s n2) 2!catA cat_uniq. apply/andP; split. by rewrite /= !inE /= negb_or andbT eq_sym (simple_neg Hg) //=n1n2 /= (simple_neg Hg). apply/andP; split. apply/hasP; case => x. rewrite in_cons. case/orP => [/eqP ->{x}|]. rewrite /= !inE. case/orP => [/eqP m'2n1|]. suff : ucycle g [:: m; n2; n1] by apply acyclic_g. apply/andP; split; first by rewrite /= andbT Hn2 /= andbC symmetric_g Hn1 /= -m'2n1. by rewrite /= !inE negb_or /= (simple_neg Hg) //= (simple_neg Hg) //= eq_sym n1n2. rewrite orbC eq_sym (negbTE (simple_neg _ n2m'2)) //= => /eqP m'2m. by move: Hm'2; rewrite m'2m in_setD1 eqxx. rewrite mem_cat => /orP[Hx|]. rewrite !inE => /orP[/eqP xn1|]. move: Hx; rewrite {}xn1 {x} => Hx. case/splitPr : Hx => k1 k2 in Hk' Hunk k'k Hkast. suff : ucycle g [:: n1, m, n2, m'2 & k1] by apply acyclic_g. apply uniq_path_ucycle_extend_2 => //. by move: Hm'2; rewrite in_setD1 => /andP[]. by move: Hk'; rewrite -(cat1s n1) catA cats1 cat_path => /andP[]. by move: Hunk; rewrite -cat_cons cat_uniq => /and3P[]. case/orP => [/eqP xm|/eqP xn2]. move: Hx; rewrite {}xm {x} => Hx. case/splitPr : Hx => k1 k2 in Hk' Hunk k'k Hkast. suff : ucycle g [:: m, n2, m'2 & k1] by apply acyclic_g. move: Hk'; rewrite -[in X in X -> _](cat1s m) catA cat_path cats1 => /andP[Hk' _]. move: Hunk; rewrite -[in X in X -> _](cat1s m'2) -[in X in X -> _](cat1s m). rewrite 2!catA cat_uniq cats1 => /and3P[Hunk _ _]. exact: uniq_path_ucycle_extend_1 Hk' Hunk. by move/path_except_notin : Hk'; rewrite -xn2 Hx. rewrite mem_rev => /mem_belast; rewrite inE => /orP[/eqP ->{x}|xl']. rewrite !inE /= => /orP[|]. apply/negP; by rewrite (simple_neg Hg) // symmetric_g. case/orP => [/eqP m'1m|/eqP m'1n2]; first by move: Hm'1; rewrite m'1m in_setD1 eqxx. suff : ucycle g [:: m; n2; n1] by apply acyclic_g. rewrite /ucycle /= !andbT !inE Hn2 /= symmetric_g -{1}m'1n2 n1m'1 /= symmetric_g Hn1 /=. by rewrite (negbTE (simple_neg _ Hn2)) //= (simple_neg Hg) //= eq_sym. rewrite !inE /= => /orP[|]. apply/negP; apply: contraTN xl' => /eqP ->; exact: path_except_notin Hl'. case/orP => [/eqP xm|/eqP xn2]. move: xl'; rewrite {}xm {x} => Hx. case/splitPr : Hx => l1 l2 in Hl' Hunl l'l Hlast. suff : ucycle g [:: m, n1, m'1 & l1] by apply acyclic_g. move: Hl'; rewrite -[in X in X -> _](cat1s m) catA cat_path cats1 => /andP[Hl' _]. move: Hunl; rewrite -[in X in X -> _](cat1s m'1) -[in X in X -> _](cat1s m). rewrite 2!catA cat_uniq cats1 => /and3P[Hunl _ _]. exact: uniq_path_ucycle_extend_1 Hl' Hunl. move: xl'; rewrite xn2 => Hx. case/splitPr : Hx => l1 l2 in Hl' Hunl l'l Hlast. suff : ucycle g [:: n2, m, n1, m'1 & l1] by apply acyclic_g. apply uniq_path_ucycle_extend_2 => //. by move: Hm'1; rewrite in_setD1 => /andP[]. by move: Hl'; rewrite -[in X in X -> _](cat1s n2) catA cats1 cat_path => /andP[]. by move: Hunl; rewrite -[in X in X -> _](cat1s m'1) catA cat_uniq => /andP[]. rewrite -cat_cons cat_uniq Hunk /=. apply/andP; split; last first. by move: Hunl; rewrite rev_uniq lastI rcons_uniq => /andP[]. apply/hasP; case => x. rewrite mem_rev => /mem_belast. rewrite inE => /orP[/eqP ->{x}|]. rewrite !inE. case/orP => [/eqP m'1m'2|m'1k]. suff : ucycle g [:: n2; m; n1; m'1] by apply acyclic_g. rewrite /ucycle /= symmetric_g Hn2 /= Hn1 /= n1m'1 /= !andbT symmetric_g m'1m'2 n2m'2 /=. rewrite !inE !negb_or /= eq_sym (simple_neg Hg) //= eq_sym n1n2 /= (simple_neg Hg) //=. rewrite (simple_neg Hg) //= -m'1m'2 andbC (simple_neg Hg) //=. by move: Hm'1; rewrite in_setD1 eq_sym => /andP[]. case/splitPr : m'1k => k1 k2 in Hk' Hunk k'k Hkast. suff : ucycle g [:: m'1, n1, m, n2, m'2 & k1] by apply acyclic_g. apply uniq_path_ucycle_extend_3 => //. by move: Hm'2; rewrite in_setD1 => /andP[]. by move: Hm'1; rewrite in_setD1 => /andP[]. by move: Hk'; rewrite -[in X in X -> _](cat1s m'1) catA cats1 cat_path => /andP[]. by move: Hunk; rewrite -[in X in X -> _](cat1s m'2) catA cat_uniq => /andP[]. rewrite /= inE => Hx. case/orP => [/eqP xm'2|xl']. move: Hx; rewrite xm'2 => xl'. case/splitPr : xl' => l1 l2 in Hl' Hunl l'l Hlast. suff : ucycle g [:: m'2, n2, m, n1, m'1 & l1] by apply acyclic_g. apply uniq_path_ucycle_extend_3 => //; first by rewrite eq_sym. by move: Hm'1; rewrite in_setD1 => /andP[]. by move: Hm'2; rewrite in_setD1 => /andP[]. by move: Hl'; rewrite -[in X in X -> _](cat1s m'2) catA cats1 cat_path => /andP[]. by move: Hunl; rewrite -[in X in X -> _](cat1s m'1) catA cat_uniq => /andP[]. case/splitPr : Hx => l1 l2 in Hl' Hunl l'l Hlast. case/splitPr : xl' => k1 k2 in Hk' Hunk k'k Hkast. suff : ucycle g ((x :: rev k1) ++ (m'2 :: n2 :: m :: n1 :: m'1 :: l1)). apply acyclic_g; by rewrite /= size_cat /= addnC. apply uniq_path_ucycle_cat_extend => //. by move: Hm'2; rewrite in_setD1 => /andP[]. by move: Hm'1; rewrite in_setD1 => /andP[]. by move: Hl'; rewrite -(cat1s x) catA cat_path cats1 => /andP[]. by move: Hk'; rewrite -(cat1s x) catA cat_path cats1 => /andP[]. by move: Hunl; rewrite -cat_cons cat_uniq => /andP[]. by move: Hunk; rewrite -cat_cons cat_uniq => /andP[]. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext