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)
  _p_ : positive
  Hk0 : Z.pos _p_ <= 0
  ============================
   (Pos.to_nat _p_ = 0%nat)


DEBUG:Going to execute:
apply : eq_sym ; trivial
Level 0: Backtrace:

Proof is not complete.
Level 0: Backtrace:

Proof is not complete.