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


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