Goal:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <=
    match lsp G1 vx vy with
    | Some n => n
    | None => nxy2 - 1
    end -> (Some nxy2 <= lsp G1 vx vy)%nbar)


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrcase@0> $1 $2

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1 -> nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1 ->
    (Some nxy2 <= None)%nbar)


DEBUG:Going to execute:
lia
DEBUG LTAC Evaluated term: (lsp ?G ?x ?z)

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1 -> nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1 ->
    (Some nxy2 <= None)%nbar)


DEBUG:Going to execute:
Zify.zify; xlia zchecker

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1 -> nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1 ->
    (Some nxy2 <= None)%nbar)


DEBUG:Going to execute:
Zify.zify

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1 -> nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1 ->
    (Some nxy2 <= None)%nbar)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op;
            Zify.zify_iter_specs; Zify.zify_to_euclidean_division_equations;
            Zify.zify_post_hook; zify_saturate

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1 -> nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1 ->
    (Some nxy2 <= None)%nbar)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op;
            Zify.zify_iter_specs; Zify.zify_to_euclidean_division_equations;
            Zify.zify_post_hook

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1 -> nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1 ->
    (Some nxy2 <= None)%nbar)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op;
            Zify.zify_iter_specs; Zify.zify_to_euclidean_division_equations

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1 -> nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1 ->
    (Some nxy2 <= None)%nbar)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op;
            Zify.zify_iter_specs

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1 -> nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1 ->
    (Some nxy2 <= None)%nbar)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1 -> nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1 ->
    (Some nxy2 <= None)%nbar)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1 -> nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1 ->
    (Some nxy2 <= None)%nbar)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1 -> nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  ============================
   (Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1 ->
    (Some nxy2 <= None)%nbar)


DEBUG:Going to execute:
intros

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1
  ============================
   (nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1
  ============================
   (Some nxy2 <= None)%nbar


DEBUG:Going to execute:
Zify.zify_pre_hook

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1
  ============================
   (nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1
  ============================
   (Some nxy2 <= None)%nbar


DEBUG:Going to execute:
idtac

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1
  ============================
   (nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1
  ============================
   (Some nxy2 <= None)%nbar


DEBUG:Going to execute:
zify_elim_let

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1
  ============================
   (nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n := match lsp G1 vx vy with
       | Some n => n
       | None => nxy2 - 1
       end : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1
  ============================
   (Some nxy2 <= None)%nbar


DEBUG:Going to execute:
<coq-core.plugins.zify::TRANS@3>

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1
  heq_n : n = match lsp G1 vx vy with
              | Some n => n
              | None => nxy2 - 1
              end
  ============================
   (nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1
  heq_n : n = match lsp G1 vx vy with
              | Some n => n
              | None => nxy2 - 1
              end
  ============================
   (Some nxy2 <= None)%nbar


DEBUG:Going to execute:
zify_op

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1
  heq_n : n = match lsp G1 vx vy with
              | Some n => n
              | None => nxy2 - 1
              end
  ============================
   (nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1
  heq_n : n = match lsp G1 vx vy with
              | Some n => n
              | None => nxy2 - 1
              end
  ============================
   (Some nxy2 <= None)%nbar


DEBUG:Going to execute:
<coq-core.plugins.zify::TRANS@0>

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1
  heq_n : n = match lsp G1 vx vy with
              | Some n => n
              | None => nxy2 - 1
              end
  cstr : 0 <= Z.of_nat (l' vy)
  cstr0 : 0 <= Z.of_nat (l' vx)
  ============================
   (nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1
  heq_n : n = match lsp G1 vx vy with
              | Some n => n
              | None => nxy2 - 1
              end
  cstr : 0 <= Z.of_nat (l' vy)
  cstr0 : 0 <= Z.of_nat (l' vx)
  ============================
   (Some nxy2 <= None)%nbar


DEBUG:Going to execute:
Zify.zify_iter_specs

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1
  heq_n : n = match lsp G1 vx vy with
              | Some n => n
              | None => nxy2 - 1
              end
  cstr : 0 <= Z.of_nat (l' vy)
  cstr0 : 0 <= Z.of_nat (l' vx)
  ============================
   (nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1
  heq_n : n = match lsp G1 vx vy with
              | Some n => n
              | None => nxy2 - 1
              end
  cstr : 0 <= Z.of_nat (l' vy)
  cstr0 : 0 <= Z.of_nat (l' vx)
  ============================
   (Some nxy2 <= None)%nbar


DEBUG:Going to execute:
fun => <coq-core.plugins.zify::ITER@0>

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1
  heq_n : n = match lsp G1 vx vy with
              | Some n => n
              | None => nxy2 - 1
              end
  cstr : 0 <= Z.of_nat (l' vy)
  cstr0 : 0 <= Z.of_nat (l' vx)
  ============================
   (nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1
  heq_n : n = match lsp G1 vx vy with
              | Some n => n
              | None => nxy2 - 1
              end
  cstr : 0 <= Z.of_nat (l' vy)
  cstr0 : 0 <= Z.of_nat (l' vx)
  ============================
   (Some nxy2 <= None)%nbar


DEBUG:Going to execute:
Zify.zify_to_euclidean_division_equations

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1
  heq_n : n = match lsp G1 vx vy with
              | Some n => n
              | None => nxy2 - 1
              end
  cstr : 0 <= Z.of_nat (l' vy)
  cstr0 : 0 <= Z.of_nat (l' vx)
  ============================
   (nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1
  heq_n : n = match lsp G1 vx vy with
              | Some n => n
              | None => nxy2 - 1
              end
  cstr : 0 <= Z.of_nat (l' vy)
  cstr0 : 0 <= Z.of_nat (l' vx)
  ============================
   (Some nxy2 <= None)%nbar


DEBUG:Going to execute:
lazymatch Zify.zify_convert_to_euclidean_division_equations_flag
           with
           | true =>
               Zify.zify_internal_to_euclidean_division_equations
           | false => idtac
           end

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1
  heq_n : n = match lsp G1 vx vy with
              | Some n => n
              | None => nxy2 - 1
              end
  cstr : 0 <= Z.of_nat (l' vy)
  cstr0 : 0 <= Z.of_nat (l' vx)
  ============================
   (nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1
  heq_n : n = match lsp G1 vx vy with
              | Some n => n
              | None => nxy2 - 1
              end
  cstr : 0 <= Z.of_nat (l' vy)
  cstr0 : 0 <= Z.of_nat (l' vx)
  ============================
   (Some nxy2 <= None)%nbar


DEBUG:Going to execute:
Zify.zify_convert_to_euclidean_division_equations_flag

Goals:
  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  nxy1 : Z
  eqlsp1 : lsp G1 vx vy = Some nxy1
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy1
  heq_n : n = match lsp G1 vx vy with
              | Some n => n
              | None => nxy2 - 1
              end
  cstr : 0 <= Z.of_nat (l' vy)
  cstr0 : 0 <= Z.of_nat (l' vx)
  ============================
   (nxy2 <= nxy1)

  
  G1 : t
  G2 : t
  H : acyclic_no_loop G1
  H0 : invariants G1
  hext : forall l1 : labelling,
         correct_labelling G1 l1 ->
         exists l2 : labelling,
           correct_labelling G2 l2 /\
           (forall v : VSet.elt, VSet.In v (V G1) -> l1 v = l2 v)
  vx : VSet.elt
  vy : VSet.elt
  hvx : VSet.In vx (V G1)
  hvy : VSet.In vy (V G1)
  nxy2 : Z
  eqlsp2 : lsp G2 vx vy = Some nxy2
  n : Z
  hbound : (lsp G1 vx vy <= Some n)%nbar
  hl : correct_labelling G1 (RelabelWrtEdge.l' G1 vx vy n)
  l' : labelling
  hl' : correct_labelling G2 l'
  ll' : forall v : VSet.elt,
        VSet.In v (V G1) -> RelabelWrtEdge.l' G1 vx vy n v = l' v
  h : Z.of_nat (l' vx) + nxy2 <= Z.of_nat (l' vy)
  eqlsp1 : lsp G1 vx vy = None
  hdiff : Z.of_nat (l' vy) - Z.of_nat (l' vx) <= nxy2 - 1
  heq_n : n = match lsp G1 vx vy with
              | Some n => n
              | None => nxy2 - 1
              end
  cstr : 0 <= Z.of_nat (l' vy)
  cstr0 : 0 <= Z.of_nat (l' vx)
  ============================
   (Some nxy2 <= None)%nbar


DEBUG:Going to execute:
constr:(false)