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
  n : nat
  IHn : P (max - n)
  n0 : ~ (Z.of_nat max <= Z.of_nat n)%Z
  cstr : (0 <= Z.of_nat n)%Z
  cstr0 : (0 <= Z.of_nat max)%Z
  ============================
   ((Z.max 0 (Z.of_nat max - (Z.of_nat n + 1)) + 1)%Z =
    Z.max 0 (Z.of_nat max - Z.of_nat n))


DEBUG:Going to execute:
Zify.zify_iter_specs