## ยง Less than versus Less than or equals over Z

- If we have a theorem whose hypotheses and goal are of the form
`a <= b - 1`

for `a, b`

integers, is it always safe to replace these with `a < b`

? Shockingly, no! - Consider the theorem:
`(a <= n - 1) => (2a <= 2n - 2)`

. - When we lose the information to
`. < .`

, it becomes `(a < n) => (2a < 2n - 1)`

. - But this can't be proved, because the best we can do is
`(a < n) => 2a < 2n`

! - The key reason is that even though
`(a < n) <-> (a <= n - 1)`

is an equivalence, we can't always rewrite with an equivalence under an inequality! - Said differently,
`a <= n - 1`

is equivalent to `a < n`

, but once we start performing *algebra *on these, we start seeing the difference. - This came up in the context of delinearization. I was trying to prove that if
`i < N`

and `j < M`

, then `iM + j < NM`

. - This proof, while state in terms of
`<`

, actually needs us to go through `<=`

: -
`i <= (N - !)`

, so `iM <= NM - M`

, so `iM + j <= (NM - M) + (M - 1)`

, which means `iM + j <= M - 1`

, or `iM < M`

.