# 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`.

source
instance Int.instIsStrictOrderedRing :
IsStrictOrderedRing ℤ

### Miscellaneous lemmas #

source
theorem Int.isCompl_even_odd :
IsCompl {n : ℤ | Even n} {n : ℤ | Odd n}
source
@[simp]
theorem Nat.cast_natAbs {α : Type u_1} [AddGroupWithOne α] (n : ℤ) :
↑n.natAbs = ↑|n|
source
theorem Int.two_le_iff_pos_of_even {m : ℤ} (even : Even m) :
2 ≤ m ↔ 0 < m
source
theorem Int.add_two_le_iff_lt_of_even_sub {m n : ℤ} (even : Even (n - m)) :
m + 2 ≤ n ↔ m < n
source
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.