fact: Definition dfs' dfs1 dfs' (roots : {set V}) e := if [pick x in roots] isn't Some x then (infty, e) else let roots' := roots :\ x in let: (m1, e1) := if [|| x \in stack e | x \in blacks e] then (rank x (stack e), e) else dfs1 x e in let: (m2, e2) := dfs' roots' e1 in (minn m1 m2, e2).
imports: mathcomp(all_ssreflect) bigmin extra