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:
split
DEBUG LTAC Evaluated term: Z.eq_dec
DEBUG LTAC Evaluated term: V.eq_dec