proposition: Lemma pre_dfs_subroots (roots roots' : {set V}) e : roots' \subset roots -> pre_dfs roots e -> pre_dfs roots' e.
proof: Proof. move=> sub_roots [to_roots [e_wf e_gwf black_sccs Nbw]]; split=> //. by move=> x x_gray y y_roots'; rewrite to_roots //; apply: subsetP y_roots'. Qed.
imports: mathcomp(all_ssreflect) bigmin extra