proposition: Lemma tarjan_rec_is_correct : tarjan_rec N setT e0 = (infty, Env setT [::] gsccs).
proof: Proof. have := @tarjan_rec_terminates N setT e0; rewrite /dfs'_correct. case: tarjan_rec => [m e] []. - by rewrite ?leq_add ?leq_mul ?max_card. - split=> //. + by move=> x; rewrite grays0 inE. + by split=> //; rewrite /= ?cover0 ?grays0 ?set0D ?setU0. + by move=> x; rewrite inE. + apply/setP=> y; rewrite !inE /= subset0 andbC; case: eqP => //= ->. by have /and3P [_ _ /negPf->] := sccs_partition edge. rewrite subTset => /eqP blackse [[[stack_wf _ _] _ _]]. rewrite grays0 => grayse; rewrite grayse setU0 in blackse. rewrite /black_gsccs /= blackse => sccse _ [_ minfty _]. have {}sccse: esccs e = gsccs. by apply/setP=> scc; rewrite sccse inE subsetT andbT. have stacke : stack e = [::]. have := stack_wf; rewrite grayse blackse sccse cover_sccs set0U setDv. by case: stack => // x s /setP /(_ x); rewrite !inE eqxx. congr (_, _); first by case: minfty => // [[x _ [y xy]]]; rewrite stacke. by case: e blackse sccse stacke {stack_wf grayse minfty} => //= *; congr Env. Qed.
imports: mathcomp(all_ssreflect) extra