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


DEBUG:Going to execute:
trivial; hnf; intros; (solve
            [ do
            ![ solve
             [ trivial | apply : eq_sym ; trivial ]
             | discriminate
             | contradiction
             | Ltac.split ]
            | case not_locked_false_eq_true; Ltac.assumption
            | match goal with
              | H:~ _ |- _ => solve [ case H; trivial ]
              end ])