Goal:
    n : Z  m : Z  comp : (n ?= m) = Eq
  ============================
   (n <= m)%Z


DEBUG:Going to execute:
destruct (Z.compare_spec n m); subst