proposition: Lemma cover_subgraph_succ2_D1 (Hg : simple g) (m n : V) (gmn : g m n) : cover (subgraph_succ2_D1 gmn) = (subgraph g m n) :\ m.
proof: Proof. apply/setP => v. rewrite /cover. apply/bigcupP => /=. rewrite 3!inE. case: ifP. case/andP => vm. case/andP => gnm. case/connectP => p. case/shortenP => p' Hpath Hun p'p Hlast. rewrite /subgraph_succ2_D1. destruct p' as [|n' t]. by rewrite Hlast eqxx in vm. rewrite /= in Hpath. case/andP : Hpath; rewrite {1}exceptE => /and3P[] gmn' mn n'n Hpath. rewrite /= in Hlast. exists (n' |: \bigcup_(m' in successors g n' :\ m) (subgraph g m' n')). apply/imsetP. exists n' => //. by rewrite !inE n'n. rewrite !inE. case/boolP : (v == n') => // vn' /=. apply/bigcupP. destruct t as [|m' t]. by rewrite Hlast eqxx in vn'. rewrite /= in Hlast. rewrite /= in Hpath. case/andP : Hpath; rewrite {1}exceptE => /and3P[] gn'm' _ m'n Hpath. exists m'. rewrite !inE gn'm' andbT; apply/eqP => ?; subst m'. by rewrite /= !inE eqxx orbT /= in Hun. rewrite !inE /subgraph /= gn'm' /=. apply/connectP. exists t => //. apply: sub_path_except Hpath => //. by rewrite (simple_neg Hg). move: Hun; by rewrite /= => /and4P[_]; rewrite inE negb_or => /andP[]. move/negbT. rewrite negb_and negbK. case/orP. move/eqP => ?; subst m. case => vs. rewrite /subgraph_succ2_D1. case/imsetP => n' Hn' ->. rewrite !inE. case/orP. by apply/negP; apply: contraTN Hn' => /eqP ->; rewrite !inE (negbTE (Hg n')) andbF. case/bigcupP => m' Hm'. rewrite /subgraph !inE. case/andP => gn'm' abs. rewrite !inE in Hn', Hm'. case/andP : Hn' => H1 H2. case/andP : Hm' => H3 H4. move: acyclic_g. rewrite /acyclic. case/connectP : abs => l. case/shortenP => l' Hpath Hun l'l Hlast. destruct l' as [| l1 l2]. rewrite /= in Hlast; subst m'. by rewrite eqxx in H3. move/(_ [:: n', m', l1 & l2] erefl) => /=. apply. rewrite /ucycle; apply/andP; split. rewrite (cycle_path n') [l1 :: _]lock /= H4 /= -lock. by rewrite (@except_path _ _ n') ?andbT // -Hlast. rewrite [m' :: _]lock /= -{2}lock Hun andbT -lock. rewrite inE negb_or (simple_neg Hg) //=; exact: path_except_notin Hpath. rewrite negb_and symmetric_g gmn /= => H1 [vs]. rewrite /subgraph_succ2_D1. case/imsetP => n'. rewrite !inE. case/andP => n'n gmn' ->{vs}. rewrite !inE. case/orP. move/eqP=> ?; subst n'. have : connect (except g n) m v. apply/connectP; exists [:: v] => //=. by rewrite exceptE /= gmn' n'n /= 2!andbT (simple_neg Hg). by rewrite (negbTE H1). case/bigcupP => m'. rewrite 3!inE => /andP[m'm n'm']. rewrite /subgraph !inE n'm' /= => m'v. move/negP : H1; apply. have {}m'v : connect (except g n) m' v. case/connectP : m'v => l Hpath Hlast. case/shortenP : Hpath Hlast => l' Hl' Hun l'l Hlast. apply/connectP; exists l' => //. have nm' : n != m'. apply/eqP => ?; subst m'. apply: (@acyclic_g [:: m ; n ; n']) => //. rewrite /ucycle; apply/andP; split. by rewrite /path.cycle rcons_path /= gmn /= symmetric_g n'm' /= symmetric_g. by rewrite /= !inE /= eq_sym negb_or m'm /= andbT (simple_neg Hg) //= eq_sym. move: (Hl'); apply sub_path_except => //. apply/negP => nl'. case/splitPr : nl' => l1 l2 in Hl' l'l Hun Hlast. suff : (ucycle g [:: n, m, n', m' & l1]) by apply acyclic_g. apply/andP; split. rewrite /path.cycle rcons_path /= symmetric_g gmn gmn' n'm' /=. move: Hl'. by rewrite -cat1s cat_path /= => /and3P[/except_path -> /= /except_rel]. rewrite [m :: _]lock /= -lock; apply/andP; split. rewrite inE negb_or eq_sym (simple_neg Hg) //= inE negb_or eq_sym n'n /= inE negb_or nm' /=. move: Hun. rewrite -(cat1s n) -(cat1s m') uniq_catC -2!catA uniq_catCA catA cat_uniq. case/andP => Hun _; move: Hun. by rewrite -rev_uniq rev_cat uniq_catC /= mem_rev => /andP[]. rewrite [n' :: _]lock /= -lock; apply/andP; split. rewrite !inE !negb_or (simple_neg Hg) //= eq_sym m'm /=. apply/negP => ml1; case/splitPr: ml1 => l11 l12 in Hl' l'l Hun Hlast. suff : ucycle g ([:: m, n', m' & l11]) by apply acyclic_g. apply/andP; split. rewrite /path.cycle rcons_path /= gmn' n'm' /=. move: Hl'; rewrite -catA cat_path. by case/andP => /except_path -> /= /andP[] /except_rel. rewrite -(cat1s m) -(cat1s n') -(cat1s m') catA cat_uniq andbA. apply/andP; split; last first. move: Hun. by rewrite -[in X in X -> _](cat1s m') 2!catA -(catA ([:: m'] ++ l11)) cat_uniq => /andP[]. apply/andP; split; first by rewrite /= !inE (simple_neg Hg). apply/hasP; case => x. rewrite !inE. case/orP => [/eqP ->{x} | Hx ]. by rewrite (negbTE m'm) /= eq_sym (negbTE (simple_neg Hg _)). case/orP => [/eqP xm|/eqP xn']. move: Hun; rewrite -(cat1s m') -catA cat_uniq => /andP[/= _ /andP[] _]. rewrite -(cat1s m) catA cat_uniq => /andP []. by rewrite -rev_uniq rev_cat /= mem_rev -xm Hx. by move: Hl'; rewrite -catA cat_path => /andP[/path_except_notin]; rewrite -xn' Hx. rewrite [m' :: _]lock /= -lock; apply/andP; split. rewrite inE negb_or (simple_neg Hg) //=. by move: Hl'; rewrite cat_path; case/andP => /path_except_notin. rewrite -(cat1s m') catA cat_uniq in Hun; by case/andP : Hun. apply: connect_trans _ m'v. apply (@connect_trans _ _ n'). - apply connect1. by rewrite exceptE /= gmn' n'n andbT /= (simple_neg Hg). - apply connect1. rewrite exceptE /= n'm' n'n /=. apply/eqP => abs; subst m'. apply: (@acyclic_g [:: m; n'; n] erefl). by rewrite /ucycle /= gmn' n'm' symmetric_g gmn /= !inE n'n negb_or (simple_neg Hg) // eq_sym m'm. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext