Goal:
  
  n : nat
  m : nat
  k : nat
  z2 : Z
  H : z2 = Z.of_nat k
  cstr : 0 <= Z.of_nat k
  cstr0 : 0 <= Z.of_nat m
  cstr1 : 0 <= Z.of_nat n
  H2 : Z.of_nat n < Z.of_nat m /\ z2 = Z.of_nat m \/
       Z.of_nat m <= Z.of_nat n /\ z2 = 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_saturate