§ 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.