Further fine-tune equations for Int2Bytes(Int, Endianness, Signedness)

* Use `0 ==Int I` instead of a syntactic _match_ of the argument with `0`.
  This enables evaluating terms with `I ==Int 0` in the path condition.
* Remove case with literal `-1` and widen requires in equation for negative
  arguments (previously `I <Int -1`, now `I <Int 0`).

k-distribution/include/kframework/builtin/domains.md

@@ -2210,14 +2210,14 @@ module BYTES
   imports BYTES-KORE
   imports private INT
 
+  rule Int2Bytes(I::Int, _::Endianness, _)        => .Bytes
+    requires I ==Int 0
   rule Int2Bytes(I::Int, E::Endianness, Unsigned) => Int2Bytes((log2Int(I) +Int 8) /Int 8, I, E)
     requires I >Int 0 [preserves-definedness]
-  rule Int2Bytes(0, _::Endianness, _) => .Bytes
-  rule Int2Bytes(I::Int, E::Endianness, Signed) => Int2Bytes((log2Int(I) +Int 9) /Int 8, I, E)
+  rule Int2Bytes(I::Int, E::Endianness, Signed  ) => Int2Bytes((log2Int(I) +Int 9) /Int 8, I, E)
     requires I >Int 0 [preserves-definedness]
-  rule Int2Bytes(I::Int, E::Endianness, Signed) => Int2Bytes((log2Int(~Int I) +Int 9) /Int 8, I, E)
-    requires I <Int -1 [preserves-definedness]
-  rule Int2Bytes(-1, E::Endianness, Signed) => Int2Bytes(1, -1, E)
+  rule Int2Bytes(I::Int, E::Endianness, Signed  ) => Int2Bytes((log2Int(~Int I) +Int 9) /Int 8, I, E)
+    requires I <Int 0 [preserves-definedness]
 endmodule
 ```