fact: Definition post_dfs (roots : {set V}) (e e' : env) (m : nat) := [/\ [/\ wf_env e', wf_graph e', noblack_to_white e', grays e' = grays e & esccs e' = black_gsccs e'], [/\ exists2 s, stack e' = s ++ stack e & s \subset (blacks e'), blacks e \subset blacks e' & esccs e \subset esccs e' ]& [/\ forall x, x \in roots -> m <= rank x (stack e'), m = infty \/ exists2 x, x \in roots & rank_of_reachable m x (stack e') & forall y, y \in xedges (stack e') (stack e) -> m <= rank y (stack e') ] ].
imports: mathcomp(all_ssreflect) extra