Goal:
  
  P : nat -> Prop
  h : forall n : nat, (forall m : nat, m < n -> P m) -> P n
  m : nat
  hh : (Z.of_nat m < 0)%Z
  cstr : (0 <= Z.of_nat m)%Z
  ============================
   (P m)


DEBUG:Going to execute:
zify_saturate