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
  z0 : Z
  H0 : (0 < Z.of_nat max - 0)%Z /\ z0 = (Z.of_nat max - 0)%Z \/
       (Z.of_nat max - 0 <= 0)%Z /\ z0 = 0%Z
  ============================
   (z0 >= Z.of_nat max)%Z


DEBUG:Going to execute:
zify_saturate