#### 10.3.2 Properties of the `poly_int` comparisons

All “maybe” relations except `maybe_ne` are transitive, so for example:

```maybe_lt (a, b) && maybe_lt (b, c) implies maybe_lt (a, c)
```

for all a, b and c. `maybe_lt`, `maybe_gt` and `maybe_ne` are irreflexive, so for example:

```!maybe_lt (a, a)
```

is true for all a. `maybe_le`, `maybe_eq` and `maybe_ge` are reflexive, so for example:

```maybe_le (a, a)
```

is true for all a. `maybe_eq` and `maybe_ne` are symmetric, so:

```maybe_eq (a, b) == maybe_eq (b, a)
maybe_ne (a, b) == maybe_ne (b, a)
```

for all a and b. In addition:

```maybe_le (a, b) == maybe_lt (a, b) || maybe_eq (a, b)
maybe_ge (a, b) == maybe_gt (a, b) || maybe_eq (a, b)
maybe_lt (a, b) == maybe_gt (b, a)
maybe_le (a, b) == maybe_ge (b, a)
```

However:

```maybe_le (a, b) && maybe_le (b, a) does not imply !maybe_ne (a, b) [== known_eq (a, b)]
maybe_ge (a, b) && maybe_ge (b, a) does not imply !maybe_ne (a, b) [== known_eq (a, b)]
```

One example is again ‘a == 3 + 4x’ and ‘b == 1 + 5x’, where ‘maybe_le (a, b)’, ‘maybe_ge (a, b)’ and ‘maybe_ne (a, b)’ all hold. `maybe_le` and `maybe_ge` are therefore not antisymetric and do not form a partial order.

From the above, it follows that:

• All “known” relations except `known_ne` are transitive.
• `known_lt`, `known_ne` and `known_gt` are irreflexive.
• `known_le`, `known_eq` and `known_ge` are reflexive.

Also:

```known_lt (a, b) == known_gt (b, a)
known_le (a, b) == known_ge (b, a)
known_lt (a, b) implies !known_lt (b, a)  [asymmetry]
known_gt (a, b) implies !known_gt (b, a)
known_le (a, b) && known_le (b, a) == known_eq (a, b) [== !maybe_ne (a, b)]
known_ge (a, b) && known_ge (b, a) == known_eq (a, b) [== !maybe_ne (a, b)]
```

`known_le` and `known_ge` are therefore antisymmetric and are partial orders. However:

```known_le (a, b) does not imply known_lt (a, b) || known_eq (a, b)
known_ge (a, b) does not imply known_gt (a, b) || known_eq (a, b)
```

For example, ‘known_le (4, 4 + 4x)’ holds because the runtime indeterminate x is a nonnegative integer, but neither `known_lt (4, 4 + 4x)` nor `known_eq (4, 4 + 4x)` hold.