Goal:
  
  n : Z
  lx : Z
  ky' : Z
  K := if n <=? 0 then Z.max lx (Z.succ ky' - n) else Z.max lx (Z.succ ky')
    : Z
  kx' : Z
  XX : K <= kx'
  ky'pos : 0 <= ky'
  Hle'' : K + n <= ky'
  ============================
   False


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