Commit 2024-02-23 19:51 33d32d5d
View on Github →feat: Small lemmas around |a - b| and Int.natAbs (a - b) (#10027) Proves the following statements:
- if
0 ≤ a ≤ nand0 ≤ b ≤ n, then|a - b| ≤ n(similarly with|a - b| < n) 0 < |a - b|iffa ≠ b
feat: Small lemmas around |a - b| and Int.natAbs (a - b) (#10027) Proves the following statements:
0 ≤ a ≤ n and 0 ≤ b ≤ n, then |a - b| ≤ n (similarly with |a - b| < n)0 < |a - b| iff a ≠ b