fact: Definition dfs1 (dfs : {set V} -> env -> nat * env) (x : V) e := let: (m1, e1) := dfs [set y in successors x] (add_stack x e) in if m1 < sn e then (m1, add_black x e1) else (infty, add_sccs x e1).
imports: mathcomp(all_ssreflect) bigmin extra