proposition: Lemma cover_subgraph_succ_D1 (Hg : simple g) (m n : V) (gmn : g m n) : m |: cover (subgraph_succ_D1 m n) = subgraph g m n.
proof: Proof. apply/setP => v. apply/idP/idP => [|Hlhs]. rewrite in_setU1. case/orP => [/eqP ->|]. by rewrite start_in_subgraph // symmetric_g. case/bigcupP => /= vs. rewrite /subgraph_succ_D1. case/imsetP => succ_m Hsucc_m -> succ_m_m_v. rewrite /subgraph inE symmetric_g gmn /=. move: succ_m_m_v. rewrite /subgraph inE. case/andP => H1 H2. rewrite 3!inE in Hsucc_m. suff : connect (except g n) succ_m v. apply/connect_trans/connect1. rewrite exceptE /= H1 (simple_neg Hg) //=; by case/andP : Hsucc_m. case/connectP : H2 => l Hl Kl. case/shortenP : Hl => l' Hl' uniql' subpredl' in Kl. apply/connectP. exists l' => //. apply: sub_path_except (Hl') => //. case/andP : Hsucc_m; by rewrite eq_sym. apply/negP => nl'. suff : ucycle g ([:: n; m; succ_m] ++ take (index n l') l') by apply acyclic_g. apply/andP; split; last first. rewrite -cat1s -(cat1s m) -!catA catA cat_uniq; apply/and3P; split; last first. move: uniql' => /= /andP[K1 K2]. by rewrite uniq_take // ?index_mem // andbT; apply: contra K1 => /mem_take. rewrite /= !inE /= !negb_or; case/andP : Hsucc_m => -> Hsucc_m /=. rewrite eq_sym (simple_neg Hg) //=. apply/hasPn => x /= Hx; rewrite !inE negb_or; apply/andP; split; last first. move/path_except_notin : Hl'; apply: contra => /eqP <-. exact: mem_take Hx. apply: contraTN Hx => /eqP ->. by rewrite take_index. rewrite /= inE andbT; apply: contraTN nl' => /eqP ->. exact: (path_except_notin Hl'). rewrite /= symmetric_g gmn /= H1 /= rcons_path. apply/andP; split. move: Hl'; by rewrite -{1}(cat_take_drop (index n l') l') cat_path => /andP[/except_path]. move: Hl'. rewrite -{1}(cat_take_drop (index n l').+1 l') (take_nth n) // ?index_mem //. rewrite cat_path => /andP[]; rewrite exceptE rcons_path => /andP[_ /and3P[]]. by rewrite nth_index. rewrite /subgraph inE symmetric_g gmn /= in Hlhs. rewrite !inE. case/boolP : (v == m) => //= vm. apply/bigcupP => /=. rewrite /subgraph_succ_D1. case/connectP : Hlhs => t. case/shortenP. case => [_ /= _ _ ? | h t' /=]. by subst v; rewrite eqxx in vm. case/andP; rewrite {1}exceptE /= => /and3P[mh mn hn] H4 Hun t't vt. exists (subgraph g h m). by rewrite (imset_f (subgraph g ^~ m)) // !inE hn. rewrite /subgraph inE mh /=. apply/connectP; exists t' => //. case/andP : Hun; rewrite inE negb_or => /andP[m_neq_h mt'] _. exact: sub_path_except H4. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext