Goal:
    G : t
  ============================
   ((forall (x : V.t) (p : PathOf x x), weight p <= 0) <->
    (forall x : V.t, ~ (exists p : PathOf x x, weight p > 0)))


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::split@0>