Goal:
  
  G : t
  invG : invariants G
  acG : acyclic_no_loop G
  l : labelling
  Hl : correct_labelling G l
  x : V.t
  k : nat
  d := Some (Z.of_nat (k + l x)) : option Z
  Hk : (lsp G x (s G) + d <= Some 0)%nbar
  Hl0 : l (s G) = 0%nat
  Hledge : forall e : EdgeSet.elt,
           EdgeSet.In e (E G) ->
           Z.of_nat (l e..s) + e..w <= Z.of_nat (l e..t)
  s : V.t
  w : Z
  t : V.t
  he : EdgeSet.In (s, w, t) (E G)
  u := to_label (lsp G x (s, w, t)..s + d)%nbar : nat
  hs : VSet.In (s, w, t)..s (V G)
  ht : VSet.In (s, w, t)..t (V G)
  _n_ : nat
  Hledge0 : Z.of_nat (l s) + w <= Z.of_nat (l t)
  ule : (l s <= Datatypes.S _n_)%nat
  _a_ : Z
  _a1_ : Z
  ============================
   (Z.to_nat (_a_ + Z.of_nat (k + l x)) = Datatypes.S _n_ ->
    _a_ + w <= _a1_ ->
    Z.of_nat (Z.to_nat (_a_ + Z.of_nat (k + l x))) + w <=
    Z.of_nat (Z.to_nat (_a1_ + Z.of_nat (k + l x))))


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op;
            Zify.zify_iter_specs; Zify.zify_to_euclidean_division_equations;
            Zify.zify_post_hook