feat(docs): clarify rounding, division operations and update descriptions

docs/src/content/docs/book/operators.mdx

@@ -208,7 +208,9 @@ pow(2, 255) * pow(2, 255); // build error: integer overflow!
 
 #### Divide, `/` {#binary-divide}
 
-The binary slash (_division_) operator `/{:tact}` is used for integer division of two values, which truncates toward zero if the result is positive and away from zero if the result is negative. This is also called [rounding down](https://en.wikipedia.org/wiki/Rounding#Rounding_down) or rounding toward $-∞$.
+The binary slash (_division_) operator `/{:tact}` is used for integer division of two values. It rounds the result towards negative infinity, which is also known as floor division or [rounding down](https://en.wikipedia.org/wiki/Rounding#Rounding_down).
+
+The following equation holds: `x = q*y + r`, where `q` is the quotient that is always equal to `floor(x / y)` from the TVM specification, and `r` is the remainder that will have the same sign as the divisor `y` when `r` is not zero.
 
 An attempt to divide by zero results in an error with [exit code 4](/book/exit-codes#4): `Integer overflow`.
 
@@ -218,12 +220,12 @@ It can only be applied to values of type [`Int{:tact}`][int]:
 let two: Int = 2;
 two / 2; // 1
 two / 1; // 2
--1 / 5;  // -1
--1 / -5; // 0
-1 / -5;  // -1
-1 / 5;   // 0
-6 / 5;   // 1, rounding down
--6 / 5;  // -2, rounding down (toward -∞)
+-1 / 5;  // -1, because floor(-1 / 5) = floor(-0.2) = -1
+-1 / -5; // 0,  because floor(-1 / -5) = floor(0.2) = 0
+1 / -5;  // -1, because floor(1 / -5) = floor(-0.2) = -1
+1 / 5;   // 0,  because floor(1 / 5) = floor(0.2) = 0
+6 / 5;   // 1,  because floor(6 / 5) = floor(1.2) = 1
+-6 / 5;  // -2, because floor(-6 / 5) = floor(-1.2) = -2
 ```
 
 :::note

docs/src/content/docs/ref/core-math.mdx

@@ -113,7 +113,7 @@ sqrt(-1); // ERROR! Exit code 5: Integer out of expected range
 fun divc(x: Int, y: Int): Int;
 ```
 
-Computes and returns the [rounded up][round-up] result of division of the [`Int{:tact}`][int] `x` by the [`Int{:tact}`][int] `y`.
+Computes the [rounded up][round-up] result of division of the numbers `x` and `y`. This corresponds to `ceil(x / y)` from the TVM specification.
 
 Attempts to divide by `y` equal to $0$ throw an exception with [exit code 4](/book/exit-codes#4): `Integer overflow`.
 
@@ -134,7 +134,7 @@ divc(-3, 2); // -1
 fun muldivc(x: Int, y: Int, z: Int): Int;
 ```
 
-Computes and returns the [rounded up][round-up] result of `(x * y) / z{:tact}`.
+Computes the [rounded up][round-up] result of `(x * y) / z{:tact}`. This corresponds to `ceil((x * y) / z)` from the TVM specification.
 
 If the value in calculation goes beyond the range from $-2^{256}$ to $2^{256} - 1$ inclusive, or if there is an attempt to divide by `z` equal to $0$, an exception with [exit code 4](/book/exit-codes#4) is thrown: `Integer overflow`.
 
@@ -157,7 +157,9 @@ muldivc(-3, 0, 0); // ERROR! Exit code 4: Integer overflow
 fun mulShiftRight(x: Int, y: Int, z: Int): Int;
 ```
 
-Computes and returns the [rounded down][round-down] result of `(x * y) / 2^z{:tact}`. It is a more gas-efficient equivalent of performing the [bitwise shift right](/book/operators#binary-bitwise-shift-right) on the result of multiplication of [`Int{:tact}`][int] `x` by [`Int{:tact}`][int] `y`, where [`Int{:tact}`][int] `z` is the right operand of the shift.
+Computes the [rounded down][round-down] result of `(x * y) / 2^z{:tact}`. This corresponds to `floor((x * y) / 2^z)` from the TVM specification.
+
+It is a more gas-efficient equivalent of doing the [bitwise shift right](/book/operators#binary-bitwise-shift-right) on the result of multiplication of `x` and `y`, where `z` is the right operand of the shift. 
 
 If the value in calculation goes beyond the range from $-2^{256}$ to $2^{256} - 1$ inclusive, an exception with [exit code 4](/book/exit-codes#4) is thrown: `Integer overflow`.
 
@@ -180,7 +182,7 @@ mulShiftRight(5, 5, -1); // ERROR! Exit code 5: Integer out of expected range
 fun mulShiftRightRound(x: Int, y: Int, z: Int): Int;
 ```
 
-Similar to [`mulShiftRight(){:tact}`](#mulshiftright), but instead of [rounding down][round-down], the result value is rounded to the nearest integer. If there are two equally close integers, rounding is done toward the even one.
+Computes `floor((x * y) / 2^z + 0.5)` from the TVM specification. It is similar to [`mulShiftRight(){:tact}`](#mulshiftright), but instead of [rounding down][round-down], the result value is rounded to the nearest integer with results like 42.5 rounded to 43.
 
 If the value in calculation goes beyond the range from $-2^{256}$ to $2^{256} - 1$ inclusive, an exception with [exit code 4](/book/exit-codes#4) is thrown: `Integer overflow`.
 
@@ -203,7 +205,7 @@ mulShiftRightRound(5, 5, -1); // ERROR! Exit code 5: Integer out of expected ran
 fun mulShiftRightCeil(x: Int, y: Int, z: Int): Int;
 ```
 
-Similar to [`mulShiftRight(){:tact}`](#mulshiftright), but instead of [rounding down][round-down], the result value is [rounded up][round-up].
+Computes `ceil((x * y) / 2^z)` from the TVM specification. It is similar to [`mulShiftRight(){:tact}`](#mulshiftright), but instead of [rounding down][round-down], the result value is [rounded up][round-up].
 
 If the value in calculation goes beyond the range from $-2^{256}$ to $2^{256} - 1$ inclusive, an exception with [exit code 4](/book/exit-codes#4) is thrown: `Integer overflow`.