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)
  e : EdgeSet.elt
  he : EdgeSet.In e (E G)
  u := to_label (lsp G x e..s + d)%nbar : nat
  ============================
   (Nat.max (l e..s) u = u ->
    Z.of_nat (Nat.max (l e..s) u) + e..w <=
    Z.of_nat (Nat.max (l e..t) (to_label (lsp G x e..t + d)%nbar)))


DEBUG:Going to execute:
lazymatch goal with
           | |- forall x, _ =>
                 let x := fresh x in
                 intro x;
                  (let copy := fresh x in
                   have copy := x; revert x; revert copy)
           | |- let x := _ in _ =>
                 let x := fresh x in
                 intro x;
                  (let copy := fresh x in
                   pose  copy  := x; do [ unfold x in (value of copy) ];
                    revert x; revert copy)
           | |- _ =>
                 let x := fresh "_top_" in
                 move  =>x;
                  (let copy := fresh "_top" in
                   have copy := x; revert x; revert copy)
           end