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)
  H := lsp0_triangle_inequality (V G) (s G) x y n He ?Hy
    : (lsp0 (V G) (s G) x + Some n <= lsp0 (V G) (s G) y)%nbar
  ============================
   (Z.of_nat (to_label (lsp (s G) x)) + n <=
    Z.of_nat (to_label (lsp (s G) y)))


DEBUG:Going to execute:
<coq-core.plugins.ltac::clearbody@0> $1