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. - do ![split=> //; rewrite /= ?cover0 ?grays0 ?set0D ?setU0 //]; do ?by[do [move=> ?|move/setP=> ?]; rewrite ?grays0 inE]. apply/setP=> y; rewrite !inE /= subset0 andbC; case: eqP => //= ->. by have /and3P [_ _ /negPf->]:= sccs_partition edge. move=> [[stack_wf _ _] _ _] sccse /subenv_grays grayse. rewrite (eqP _ : \bigcup_(x in _) _ = setT) ?setDT => [whe ->|]; last first. rewrite -subTset; apply/subsetP=> y _; apply/bigcupP. by exists y; rewrite ?mem_wreach. have blackse : blacks e = setT. move/eqP: whe; rewrite whitesE grayse grays0 set0U. by rewrite -subset0 subCset setC0 subTset => /eqP. rewrite /black_gsccs blackse ?grayse ?grays0 ?setTD ?set0U// in sccse stack_wf. have {}sccse: esccs e = gsccs. by apply/setP=> scc; rewrite sccse inE subsetT andbT. have stacke : stack e = [::]. have := stack_wf; rewrite sccse cover_sccs setCT. by case: stack => // x s /(_ x); rewrite !inE eqxx. congr (_, _); last by case: (e) blackse sccse stacke => //= *; congr Env. by rewrite big1=> // x _; apply/val_inj; rewrite stacke /= ord_rank ?rank_infty. Qed.
imports: mathcomp(all_ssreflect) bigmin extra