Goal:
  
  x : nat
  y : nat
  x0 : nat
  y0 : nat
  H0 : (Z.of_nat x0 <= Z.of_nat y0)%Z
  H : Z.of_nat x = Z.of_nat y
  cstr : (0 <= Z.of_nat y)%Z
  cstr0 : (0 <= Z.of_nat y0)%Z
  cstr1 : (0 <= Z.of_nat x)%Z
  cstr2 : (0 <= Z.of_nat x0)%Z
  ============================
   (Z.of_nat x + Z.of_nat x0 <= Z.of_nat y + Z.of_nat y0)%Z


DEBUG:Going to execute:
zify_saturate