proposition: Theorem tarjan_correct : tarjan = gsccs.
proof: Proof. rewrite /tarjan mulnSr; case: rec_terminates. - by rewrite visited0 setC0 cardsT. - constructor; rewrite /= ?sub0set// => x; rewrite !ffunE//. + by rewrite ltnNge leqW//. + by rewrite gtn_eqF// /cover big_set0 inE. + by move=> y; rewrite !ffunE//= andbC ltnNge leqW// ?max_card. - by move=> y; rewrite !inE !ffunE/= ltnNge leqW// max_card. move=> _ _ e -> _ e_wf _ [_]; rewrite stack0 setD0. have [stacke _|[x xe]] := set_0Vmem (stack e); last first. by move=> /(_ _ xe)[?]; rewrite inE. rewrite visited0 set0U setC0 nextsT => visitede. have numE x : num e x = infty. apply/eqP; have /setP/(_ x) := visitede. by rewrite visitedE// stacke set0U !inE -num_sccs. apply/eqP; rewrite eqEsubset sub_gsccs//=; apply/subsetP => _/imsetP[/=x _->]. have: x \in cover (esccs e) by rewrite -num_sccs ?numE//. move=> /bigcupP [C Csccs /(def_scc (subsetP (sub_gsccs e_wf) _ Csccs))] eqC. rewrite -eqC (_ : [set _ in _ | _] = gscc_of x)// in Csccs *. by apply/setP => y; rewrite !inE mem_scc /=. Qed.
imports: mathcomp(all_ssreflect) extra_nocolors