Goal:
  
  G : t
  invG : invariants G
  acG : acyclic_no_loop G
  x : V.t
  y : V.t
  hx : VSet.In x (V G)
  hy : VSet.In y (V G)
  nxy : Z
  hxy : (lsp G x y <= Some nxy)%nbar
  z1 : Nbar.t
  z2 : Nbar.t
  ============================
   ((z1 <= z2)%nbar -> (to_label z1 <= to_label z2)%nat)


DEBUG:Going to execute:
move : z1 z2  => [[|?|?]|] [[|?|?]|] //=