Goal:
    n : Z  H : (0 <= n)%Z
  ============================
   True


DEBUG:Going to execute:
idtac

Goals:
    n : Z  z : Z  H : (0 <= n)%Z
  ============================
   (z <= n + z)%Z

    n : Z  H : (0 <= n)%Z
  ============================
   True


DEBUG:Going to execute:
Zify.zify_post_hook

Goals:
    n : Z  z : Z  H : (0 <= n)%Z
  ============================
   (z <= n + z)%Z

    n : Z  H : (0 <= n)%Z
  ============================
   True


DEBUG:Going to execute:
idtac

Goals:
    n : Z  z : Z  H : (0 <= n)%Z
  ============================
   (z <= n + z)%Z

    n : Z  H : (0 <= n)%Z
  ============================
   True


DEBUG:Going to execute:
zify_saturate

Goals:
    n : Z  z : Z  H : (0 <= n)%Z
  ============================
   (z <= n + z)%Z

    n : Z  H : (0 <= n)%Z
  ============================
   True


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

Goals:
    n : Z  z : Z  H : (0 <= n)%Z
  ============================
   (z <= n + z)%Z

    n : Z  H : (0 <= n)%Z
  ============================
   True


DEBUG:Going to execute:
xlia zchecker

Goals:
    n : Z  z : Z  H : (0 <= n)%Z
  ============================
   (z <= n + z)%Z

    n : Z  H : (0 <= n)%Z
  ============================
   True


DEBUG:Going to execute:
<coq-core.plugins.micromega::Lia@0> $1