Goal:
  
  n : nat
  m : nat
  k : nat
  H : Z.max (Z.of_nat n) (Z.of_nat m) = Z.of_nat k
  cstr : 0 <= Z.of_nat k
  cstr0 : 0 <= Z.of_nat m
  cstr1 : 0 <= Z.of_nat n
  ============================
   (Z.of_nat n = Z.of_nat k \/ Z.of_nat m = Z.of_nat k)


DEBUG:Going to execute:
Zify.zify_iter_specs