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
  _p_ : positive
  n : nat
  H : 0 <= Z.pos _p_
  ============================
   ((Pos.to_nat _p_ + Datatypes.S n)%nat =
    Pos.to_nat (_p_ + Pos.of_succ_nat n))


DEBUG:Going to execute:
match goal with
           | H:~ _ |- _ => solve [ case H; trivial ]
           end
Level 1: Backtrace:

No such assumption.
Level 0: Backtrace:

No such assumption.
Level 0: Backtrace:

No such assumption.
Level 0: Backtrace:

No such assumption.

Goals:
  
  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
  ============================
   (forall n : nat, 0 <= 0 -> Datatypes.S n = Pos.to_nat (Pos.of_succ_nat n))

  
  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
  _p_ : positive
  ============================
   (forall n : nat,
    0 <= Z.pos _p_ ->
    (Pos.to_nat _p_ + Datatypes.S n)%nat =
    Pos.to_nat (_p_ + Pos.of_succ_nat n))


DEBUG:Going to execute:
lia
Level 0: Backtrace:

No matching clauses for match.
Level 0: Backtrace:

No applicable tactic.
Level 0: Backtrace:

No applicable tactic.
Level 0: Backtrace:

No applicable tactic.
Level 0: Backtrace:

No applicable tactic.
Level 0: Backtrace:

No applicable tactic.
Level 0: Backtrace:

No applicable tactic.
Level 0: Backtrace:

No applicable tactic.
Level 1: Backtrace:

No applicable tactic.
Level 0: Backtrace:

No applicable tactic.

Goals:
  
  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
  ============================
   (forall n : nat, 0 <= 0 -> Datatypes.S n = Pos.to_nat (Pos.of_succ_nat n))

  
  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
  _p_ : positive
  ============================
   (forall n : nat,
    0 <= Z.pos _p_ ->
    (Pos.to_nat _p_ + Datatypes.S n)%nat =
    Pos.to_nat (_p_ + Pos.of_succ_nat n))


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

Goals:
  
  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
  ============================
   (forall n : nat, 0 <= 0 -> Datatypes.S n = Pos.to_nat (Pos.of_succ_nat n))

  
  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
  _p_ : positive
  ============================
   (forall n : nat,
    0 <= Z.pos _p_ ->
    (Pos.to_nat _p_ + Datatypes.S n)%nat =
    Pos.to_nat (_p_ + Pos.of_succ_nat n))


DEBUG:Going to execute:
Zify.zify

Goals:
  
  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
  ============================
   (forall n : nat, 0 <= 0 -> Datatypes.S n = Pos.to_nat (Pos.of_succ_nat n))

  
  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
  _p_ : positive
  ============================
   (forall n : nat,
    0 <= Z.pos _p_ ->
    (Pos.to_nat _p_ + Datatypes.S n)%nat =
    Pos.to_nat (_p_ + Pos.of_succ_nat n))


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:
  
  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
  ============================
   (forall n : nat, 0 <= 0 -> Datatypes.S n = Pos.to_nat (Pos.of_succ_nat n))

  
  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
  _p_ : positive
  ============================
   (forall n : nat,
    0 <= Z.pos _p_ ->
    (Pos.to_nat _p_ + Datatypes.S n)%nat =
    Pos.to_nat (_p_ + Pos.of_succ_nat n))


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:
  
  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
  ============================
   (forall n : nat, 0 <= 0 -> Datatypes.S n = Pos.to_nat (Pos.of_succ_nat n))

  
  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
  _p_ : positive
  ============================
   (forall n : nat,
    0 <= Z.pos _p_ ->
    (Pos.to_nat _p_ + Datatypes.S n)%nat =
    Pos.to_nat (_p_ + Pos.of_succ_nat n))


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:
  
  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
  ============================
   (forall n : nat, 0 <= 0 -> Datatypes.S n = Pos.to_nat (Pos.of_succ_nat n))

  
  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
  _p_ : positive
  ============================
   (forall n : nat,
    0 <= Z.pos _p_ ->
    (Pos.to_nat _p_ + Datatypes.S n)%nat =
    Pos.to_nat (_p_ + Pos.of_succ_nat n))


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

Goals:
  
  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
  ============================
   (forall n : nat, 0 <= 0 -> Datatypes.S n = Pos.to_nat (Pos.of_succ_nat n))

  
  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
  _p_ : positive
  ============================
   (forall n : nat,
    0 <= Z.pos _p_ ->
    (Pos.to_nat _p_ + Datatypes.S n)%nat =
    Pos.to_nat (_p_ + Pos.of_succ_nat n))


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

Goals:
  
  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
  ============================
   (forall n : nat, 0 <= 0 -> Datatypes.S n = Pos.to_nat (Pos.of_succ_nat n))

  
  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
  _p_ : positive
  ============================
   (forall n : nat,
    0 <= Z.pos _p_ ->
    (Pos.to_nat _p_ + Datatypes.S n)%nat =
    Pos.to_nat (_p_ + Pos.of_succ_nat n))


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

Goals:
  
  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
  ============================
   (forall n : nat, 0 <= 0 -> Datatypes.S n = Pos.to_nat (Pos.of_succ_nat n))

  
  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
  _p_ : positive
  ============================
   (forall n : nat,
    0 <= Z.pos _p_ ->
    (Pos.to_nat _p_ + Datatypes.S n)%nat =
    Pos.to_nat (_p_ + Pos.of_succ_nat n))


DEBUG:Going to execute:
intros; Zify.zify_pre_hook

Goals:
  
  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
  ============================
   (forall n : nat, 0 <= 0 -> Datatypes.S n = Pos.to_nat (Pos.of_succ_nat n))

  
  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
  _p_ : positive
  ============================
   (forall n : nat,
    0 <= Z.pos _p_ ->
    (Pos.to_nat _p_ + Datatypes.S n)%nat =
    Pos.to_nat (_p_ + Pos.of_succ_nat n))


DEBUG:Going to execute:
intros

Goals:
  
  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
  n : nat
  H : 0 <= 0
  ============================
   (Datatypes.S n = Pos.to_nat (Pos.of_succ_nat n))

  
  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
  _p_ : positive
  n : nat
  H : 0 <= Z.pos _p_
  ============================
   ((Pos.to_nat _p_ + Datatypes.S n)%nat =
    Pos.to_nat (_p_ + Pos.of_succ_nat n))


DEBUG:Going to execute:
Zify.zify_pre_hook

Goals:
  
  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
  n : nat
  H : 0 <= 0
  ============================
   (Datatypes.S n = Pos.to_nat (Pos.of_succ_nat n))

  
  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
  _p_ : positive
  n : nat
  H : 0 <= Z.pos _p_
  ============================
   ((Pos.to_nat _p_ + Datatypes.S n)%nat =
    Pos.to_nat (_p_ + Pos.of_succ_nat n))


DEBUG:Going to execute:
idtac

Goals:
  
  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
  n : nat
  H : 0 <= 0
  ============================
   (Datatypes.S n = Pos.to_nat (Pos.of_succ_nat n))

  
  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
  _p_ : positive
  n : nat
  H : 0 <= Z.pos _p_
  ============================
   ((Pos.to_nat _p_ + Datatypes.S n)%nat =
    Pos.to_nat (_p_ + Pos.of_succ_nat n))


DEBUG:Going to execute:
zify_elim_let

Goals:
  
  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
  n : nat
  H : 0 <= 0
  ============================
   (Datatypes.S n = Pos.to_nat (Pos.of_succ_nat n))

  
  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
  _p_ : positive
  n : nat
  H : 0 <= Z.pos _p_
  ============================
   ((Pos.to_nat _p_ + Datatypes.S n)%nat =
    Pos.to_nat (_p_ + Pos.of_succ_nat n))


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

Goals:
  
  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
  n : nat
  H : 0 <= 0
  ============================
   (Datatypes.S n = Pos.to_nat (Pos.of_succ_nat n))

  
  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
  _p_ : positive
  n : nat
  H : 0 <= Z.pos _p_
  ============================
   ((Pos.to_nat _p_ + Datatypes.S n)%nat =
    Pos.to_nat (_p_ + Pos.of_succ_nat n))


DEBUG:Going to execute:
zify_op

Goals:
  
  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
  n : nat
  H : 0 <= 0
  ============================
   (Datatypes.S n = Pos.to_nat (Pos.of_succ_nat n))

  
  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
  _p_ : positive
  n : nat
  H : 0 <= Z.pos _p_
  ============================
   ((Pos.to_nat _p_ + Datatypes.S n)%nat =
    Pos.to_nat (_p_ + Pos.of_succ_nat n))


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

Goals:
  
  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
  n : nat
  H : 0 <= 0
  cstr : 0 <= Z.of_nat n
  ============================
   (Z.of_nat n + 1 = Z.of_nat n + 1)

  
  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
  _p_ : positive
  n : nat
  H : 0 <= Z.pos _p_
  cstr : 0 <= Z.of_nat n
  cstr0 : 0 < Z.pos _p_
  ============================
   (Z.pos _p_ + (Z.of_nat n + 1) = Z.pos _p_ + (Z.of_nat n + 1))


DEBUG:Going to execute:
Zify.zify_iter_specs

Goals:
  
  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
  n : nat
  H : 0 <= 0
  cstr : 0 <= Z.of_nat n
  ============================
   (Z.of_nat n + 1 = Z.of_nat n + 1)

  
  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
  _p_ : positive
  n : nat
  H : 0 <= Z.pos _p_
  cstr : 0 <= Z.of_nat n
  cstr0 : 0 < Z.pos _p_
  ============================
   (Z.pos _p_ + (Z.of_nat n + 1) = Z.pos _p_ + (Z.of_nat n + 1))


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

Goals:
  
  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
  n : nat
  H : 0 <= 0
  cstr : 0 <= Z.of_nat n
  ============================
   (Z.of_nat n + 1 = Z.of_nat n + 1)

  
  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
  _p_ : positive
  n : nat
  H : 0 <= Z.pos _p_
  cstr : 0 <= Z.of_nat n
  cstr0 : 0 < Z.pos _p_
  ============================
   (Z.pos _p_ + (Z.of_nat n + 1) = Z.pos _p_ + (Z.of_nat n + 1))


DEBUG:Going to execute:
Zify.zify_to_euclidean_division_equations

Goals:
  
  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
  n : nat
  H : 0 <= 0
  cstr : 0 <= Z.of_nat n
  ============================
   (Z.of_nat n + 1 = Z.of_nat n + 1)

  
  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
  _p_ : positive
  n : nat
  H : 0 <= Z.pos _p_
  cstr : 0 <= Z.of_nat n
  cstr0 : 0 < Z.pos _p_
  ============================
   (Z.pos _p_ + (Z.of_nat n + 1) = Z.pos _p_ + (Z.of_nat n + 1))


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:
  
  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
  n : nat
  H : 0 <= 0
  cstr : 0 <= Z.of_nat n
  ============================
   (Z.of_nat n + 1 = Z.of_nat n + 1)

  
  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
  _p_ : positive
  n : nat
  H : 0 <= Z.pos _p_
  cstr : 0 <= Z.of_nat n
  cstr0 : 0 < Z.pos _p_
  ============================
   (Z.pos _p_ + (Z.of_nat n + 1) = Z.pos _p_ + (Z.of_nat n + 1))


DEBUG:Going to execute:
Zify.zify_convert_to_euclidean_division_equations_flag

Goals:
  
  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
  n : nat
  H : 0 <= 0
  cstr : 0 <= Z.of_nat n
  ============================
   (Z.of_nat n + 1 = Z.of_nat n + 1)

  
  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
  _p_ : positive
  n : nat
  H : 0 <= Z.pos _p_
  cstr : 0 <= Z.of_nat n
  cstr0 : 0 < Z.pos _p_
  ============================
   (Z.pos _p_ + (Z.of_nat n + 1) = Z.pos _p_ + (Z.of_nat n + 1))


DEBUG:Going to execute:
constr:(false)