Goal:
  
  G : t
  HI : invariants
  HG : acyclic_no_loop
  x : V.t
  n : Z
  y : V.t
  He : EdgeSet.In (x, n, y) (E G)
  xl : Z
  eq : lsp (s G) x = Some xl
  pos : 0 <= xl
  ============================
   ((Some xl + Some n <= lsp (s G) y)%nbar ->
    xl + n <= Z.of_nat (to_label (lsp (s G) y)))


DEBUG:Going to execute:
destruct (Z_of_to_label_s y) as [yl [eq' [ylpos ->]]]
DEBUG LTAC Evaluated term: eq
DEBUG LTAC Evaluated term: eq
DEBUG LTAC Evaluated term: eq
DEBUG LTAC Evaluated term: (edges_vertices (x, n, y) He)

Goals:
  
  G : t
  HI : invariants
  HG : acyclic_no_loop
  x : V.t
  n : Z
  y : V.t
  He : EdgeSet.In (x, n, y) (E G)
  xl : Z
  eq : lsp (s G) x = Some xl
  pos : 0 <= xl
  ============================
   (VSet.In y (V G))

  
  G : t
  HI : invariants
  HG : acyclic_no_loop
  x : V.t
  n : Z
  y : V.t
  He : EdgeSet.In (x, n, y) (E G)
  xl : Z
  eq : lsp (s G) x = Some xl
  pos : 0 <= xl
  yl : Z
  eq' : lsp (s G) y = Some yl
  ylpos : 0 <= yl
  ============================
   ((Some xl + Some n <= lsp (s G) y)%nbar -> xl + n <= yl)


DEBUG:Going to execute:
rewrite ?eq'
DEBUG LTAC Evaluated term: (Z_of_to_label_s y)