proposition: Lemma cover_subgraph_succ n : cover ([set n] |: subgraph_succ n) = [set v | connect g n v].
proof: Proof. apply/setP => v; rewrite inE. apply/idP/idP => [|nv]. case/bigcupP => /= s; rewrite 2!inE => /orP[/eqP ->|]. rewrite inE => /eqP ->; exact: connect0. case/imsetP => w; rewrite inE => nw ->; exact: subgraph_connect. apply/bigcupP => /=. case/connectP : nv => t' /shortenP[t nt uniq_nt _] ->{v t'}. case: t => [|h t] in nt uniq_nt *. by exists [set n]; rewrite !inE // eqxx. exists (subgraph g h n). rewrite inE /subgraph_succ (imset_f ((subgraph g)^~ n)) ?orbT //. rewrite inE; rewrite /= in nt; by case/andP : nt. rewrite inE /=. rewrite /= in nt. case/andP : nt => -> ht /=. apply/connectP; exists t => //; apply path_except => //. by rewrite /= in uniq_nt; case/andP : uniq_nt. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext