The integers form a linear ordered ring

This file contains:

• instances on ℤ. The stronger one is Int.instLinearOrderedCommRing.
• basic lemmas about integers that involve order properties.

Recursors

• Int.rec: Sign disjunction. Something is true/defined on ℤ if it's true/defined for nonnegative and for negative values. (Defined in core Lean 3)
• Int.inductionOn: Simple growing induction on positive numbers, plus simple decreasing induction on negative numbers. Note that this recursor is currently only Prop-valued.
• Int.inductionOn': Simple growing induction for numbers greater than b, plus simple decreasing induction on numbers less than b.

instance Int.instZeroLEOneClass : ZeroLEOneClass ℤ

instance Int.instIsStrictOrderedRing : IsStrictOrderedRing ℤ

Miscellaneous lemmas

theorem Int.isCompl_even_odd : IsCompl {n : ℤ | Even n} {n : ℤ | Odd n}

theorem Nat.cast_natAbs {α : Type u_1} [AddGroupWithOne α] (n : ℤ) : ↑n.natAbs = ↑|n|

theorem Int.two_le_iff_pos_of_even {m : ℤ} (even : Even m) : 2 ≤ m ↔ 0 < m

theorem Int.add_two_le_iff_lt_of_even_sub {m n : ℤ} (even : Even (n - m)) : m + 2 ≤ n ↔ m < n

theorem Nat.exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le (p q n : ℕ) (dvd : p.gcd q ∣ n) (le : p.pred * q.pred ≤ n) : ∃ (a : ℕ) (b : ℕ), a * p + b * q = n

If the gcd of two natural numbers p and q divides a third natural number n, and if n is at least (p - 1) * (q - 1), then n can be represented as an ℕ-linear combination of p and q.

TODO: show that if p.gcd q = 1 and 0 ≤ n ≤ (p - 1) * (q - 1) - 1 = N, then n is representable iff N - n is not. In particular N is not representable, solving the coin problem for two coins: https://en.wikipedia.org/wiki/Coin_problem#n_=_2.