Goal:
  
  max : nat
  P : nat -> Prop
  hmax : forall n : nat, n >= max -> P n
  hS : forall n : nat, n < max -> P (S n) -> P n
  cstr : (0 <= Z.of_nat max)%Z
  ============================
   (Z.max 0 (Z.of_nat max - 0) >= Z.of_nat max)%Z


DEBUG:Going to execute:
fun => <coq-core.plugins.zify::ITER@0>