Goal:
  
  G : t
  l : labelling
  x : V.t
  y : V.t
  e : EdgeOf x y
  Hl : Z.of_nat (l x) + e.π1 <= Z.of_nat (l y)
  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) + (e.π1 + weight p) <= Z.of_nat (l z))


DEBUG:Going to execute:
intros