Goal:
  
  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


DEBUG:Going to execute:
idtac
DEBUG LTAC Evaluated term: false
DEBUG LTAC Evaluated term: false
Level 2: Zify.zify_convert_to_euclidean_division_equations_flag
 has value 
false

Level 2: Zify.zify_convert_to_euclidean_division_equations_flag
 has value 
false