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 num e x != 0 then (num e x, e) else dfs1 x e in let: (m2, e2) := dfs roots' e1 in (minn m1 m2, e2).
imports: mathcomp(all_ssreflect) bigmin extra