Goal:
  
  G : t
  l : labelling
  x : V.t
  y : V.t
  e : EdgeOf x y
  Hl : Z.of_nat (l (x, e.π1, y)..s) + (x, e.π1, y)..w <=
       Z.of_nat (l (x, e.π1, y)..t)
  z : V.t
  p : PathOf y z
  IHp : Z.of_nat (l y) + weight p <= Z.of_nat (l z)
  ============================
   (Z.of_nat (l x) + weight (pathOf_step e p) <= Z.of_nat (l z))


DEBUG:Going to execute:
cbn in *
DEBUG LTAC Evaluated term: (Hl (x, e.π1, y) e.π2)