Goal:
  
  n : Z
  lx : Z
  ky' : Z
  kx' : Z
  z0 : Z
  XX : z0 <= kx'
  ky'pos : 0 <= ky'
  Hle'' : z0 + n <= ky'
  H : 0 < n
  H0 : lx < ky' + 1 /\ z0 = ky' + 1 \/ ky' + 1 <= lx /\ z0 = lx
  ============================
   False


DEBUG:Going to execute:
idtac

Goals:
  
  n : Z
  lx : Z
  ky' : Z
  kx' : Z
  z0 : Z
  XX : z0 <= kx'
  ky'pos : 0 <= ky'
  Hle'' : z0 + n <= ky'
  H : n <= 0
  H0 : lx < ky' + 1 - n /\ z0 = ky' + 1 - n \/ ky' + 1 - n <= lx /\ z0 = lx
  ============================
   False

  
  n : Z
  lx : Z
  ky' : Z
  kx' : Z
  z0 : Z
  XX : z0 <= kx'
  ky'pos : 0 <= ky'
  Hle'' : z0 + n <= ky'
  H : 0 < n
  H0 : lx < ky' + 1 /\ z0 = ky' + 1 \/ ky' + 1 <= lx /\ z0 = lx
  ============================
   False


DEBUG:Going to execute:
Zify.zify_post_hook

Goals:
  
  n : Z
  lx : Z
  ky' : Z
  kx' : Z
  z0 : Z
  XX : z0 <= kx'
  ky'pos : 0 <= ky'
  Hle'' : z0 + n <= ky'
  H : n <= 0
  H0 : lx < ky' + 1 - n /\ z0 = ky' + 1 - n \/ ky' + 1 - n <= lx /\ z0 = lx
  ============================
   False

  
  n : Z
  lx : Z
  ky' : Z
  kx' : Z
  z0 : Z
  XX : z0 <= kx'
  ky'pos : 0 <= ky'
  Hle'' : z0 + n <= ky'
  H : 0 < n
  H0 : lx < ky' + 1 /\ z0 = ky' + 1 \/ ky' + 1 <= lx /\ z0 = lx
  ============================
   False


DEBUG:Going to execute:
idtac

Goals:
  
  n : Z
  lx : Z
  ky' : Z
  kx' : Z
  z0 : Z
  XX : z0 <= kx'
  ky'pos : 0 <= ky'
  Hle'' : z0 + n <= ky'
  H : n <= 0
  H0 : lx < ky' + 1 - n /\ z0 = ky' + 1 - n \/ ky' + 1 - n <= lx /\ z0 = lx
  ============================
   False

  
  n : Z
  lx : Z
  ky' : Z
  kx' : Z
  z0 : Z
  XX : z0 <= kx'
  ky'pos : 0 <= ky'
  Hle'' : z0 + n <= ky'
  H : 0 < n
  H0 : lx < ky' + 1 /\ z0 = ky' + 1 \/ ky' + 1 <= lx /\ z0 = lx
  ============================
   False


DEBUG:Going to execute:
zify_saturate

Goals:
  
  n : Z
  lx : Z
  ky' : Z
  kx' : Z
  z0 : Z
  XX : z0 <= kx'
  ky'pos : 0 <= ky'
  Hle'' : z0 + n <= ky'
  H : n <= 0
  H0 : lx < ky' + 1 - n /\ z0 = ky' + 1 - n \/ ky' + 1 - n <= lx /\ z0 = lx
  ============================
   False

  
  n : Z
  lx : Z
  ky' : Z
  kx' : Z
  z0 : Z
  XX : z0 <= kx'
  ky'pos : 0 <= ky'
  Hle'' : z0 + n <= ky'
  H : 0 < n
  H0 : lx < ky' + 1 /\ z0 = ky' + 1 \/ ky' + 1 <= lx /\ z0 = lx
  ============================
   False


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

Goals:
  
  n : Z
  lx : Z
  ky' : Z
  kx' : Z
  z0 : Z
  XX : z0 <= kx'
  ky'pos : 0 <= ky'
  Hle'' : z0 + n <= ky'
  H : n <= 0
  H0 : lx < ky' + 1 - n /\ z0 = ky' + 1 - n \/ ky' + 1 - n <= lx /\ z0 = lx
  ============================
   False

  
  n : Z
  lx : Z
  ky' : Z
  kx' : Z
  z0 : Z
  XX : z0 <= kx'
  ky'pos : 0 <= ky'
  Hle'' : z0 + n <= ky'
  H : 0 < n
  H0 : lx < ky' + 1 /\ z0 = ky' + 1 \/ ky' + 1 <= lx /\ z0 = lx
  ============================
   False


DEBUG:Going to execute:
xlia zchecker

Goals:
  
  n : Z
  lx : Z
  ky' : Z
  kx' : Z
  z0 : Z
  XX : z0 <= kx'
  ky'pos : 0 <= ky'
  Hle'' : z0 + n <= ky'
  H : n <= 0
  H0 : lx < ky' + 1 - n /\ z0 = ky' + 1 - n \/ ky' + 1 - n <= lx /\ z0 = lx
  ============================
   False

  
  n : Z
  lx : Z
  ky' : Z
  kx' : Z
  z0 : Z
  XX : z0 <= kx'
  ky'pos : 0 <= ky'
  Hle'' : z0 + n <= ky'
  H : 0 < n
  H0 : lx < ky' + 1 /\ z0 = ky' + 1 \/ ky' + 1 <= lx /\ z0 = lx
  ============================
   False


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