Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Mario Carneiro
-/
import Std.Classes.Dvd

open Nat

namespace Int

/--
`-[n+1]` is suggestive notation for `negSucc n`, which is the second constructor of
`Int` for making strictly negative numbers by mapping `n : Nat` to `-(n + 1)`.
-/
scoped notation "-[" n: ?m.2083n "+1]" => negSucc: Nat → IntnegSucc n: ?m.2083n

/- ## sign -/

/--
Returns the "sign" of the integer as another integer: `1` for positive numbers,
`-1` for negative numbers, and `0` for `0`.
-/
def sign: Int → Intsign : Int: TypeInt → Int: TypeInt
| succ: Nat → Natsucc _ => 1: ?m.79071
| 0: Int0      => 0: ?m.79250
| -[_+1] => -1: ?m.79381

/-! ## toNat' -/

/--
* If `n : Nat`, then `int.toNat' n = some n`
* If `n : Int` is negative, then `int.toNat' n = none`.
-/
def toNat': Int → Option NattoNat' : Int: TypeInt → Option: Type ?u.8169 → Type ?u.8169Option Nat: TypeNat
| (n : Nat) => some: {α : Type ?u.8266} → α → Option αsome n: Natn
| -[_+1] => none: {α : Type ?u.8278} → Option αnone

/-! ## Quotient and remainder

There are three main conventions for integer division,
referred here as the E, F, T rounding conventions.
All three pairs satisfy the identity `x % y + (x / y) * y = x` unconditionally,
and satisfy `x / 0 = 0` and `x % 0 = x`.
-/

/-! ### E-rounding division

This pair satisfies `0 ≤ mod x y < natAbs y` for `y ≠ 0`.
-/

/--
Integer division. This version of `Int.div` uses the E-rounding convention
(euclidean division), in which `Int.emod x y` satisfies `0 ≤ mod x y < natAbs y` for `y ≠ 0`
and `Int.ediv` is the unique function satisfying `emod x y + (ediv x y) * y = x`.
-/
def ediv: Int → Int → Intediv : Int: TypeInt → Int: TypeInt → Int: TypeInt
| ofNat: Nat → IntofNat m: Natm, ofNat: Nat → IntofNat n: Natn => ofNat: Nat → IntofNat (m: Natm / n: Natn)
| ofNat: Nat → IntofNat m: Natm, -[n: Natn+1]  => -ofNat: Nat → IntofNat (m: Natm / succ: Nat → Natsucc n: Natn)
| -[_+1],  0: Int0       => 0: ?m.85410
| -[m: Natm+1],  succ: Nat → Natsucc n: Natn  => -[m: Natm / succ: Nat → Natsucc n: Natn +1]
| -[m: Natm+1],  -[n: Natn+1]  => ofNat: Nat → IntofNat (succ: Nat → Natsucc (m: Natm / succ: Nat → Natsucc n: Natn))

/--
Integer modulus. This version of `Int.mod` uses the E-rounding convention
(euclidean division), in which `Int.emod x y` satisfies `0 ≤ emod x y < natAbs y` for `y ≠ 0`
and `Int.ediv` is the unique function satisfying `emod x y + (ediv x y) * y = x`.
-/
def emod: Int → Int → Intemod : Int: TypeInt → Int: TypeInt → Int: TypeInt
| ofNat: Nat → IntofNat m: Natm, n: Intn => ofNat: Nat → IntofNat (m: Natm % natAbs: Int → NatnatAbs n: Intn)
| -[m: Natm+1],  n: Intn => subNatNat: Nat → Nat → IntsubNatNat (natAbs: Int → NatnatAbs n: Intn) (succ: Nat → Natsucc (m: Natm % natAbs: Int → NatnatAbs n: Intn))

/-! ### F-rounding division

This pair satisfies `fdiv x y = floor (x / y)`.
-/

/--
Integer division. This version of `Int.div` uses the F-rounding convention
(flooring division), in which `Int.fdiv x y` satisfies `fdiv x y = floor (x / y)`
and `Int.fmod` is the unique function satisfying `fmod x y + (fdiv x y) * y = x`.
-/
def fdiv: Int → Int → Intfdiv : Int: TypeInt → Int: TypeInt → Int: TypeInt
| 0: Int0,       _       => 0: ?m.95390
| ofNat: Nat → IntofNat m: Natm, ofNat: Nat → IntofNat n: Natn => ofNat: Nat → IntofNat (m: Natm / n: Natn)
| succ: Nat → Natsucc m: Natm,  -[n: Natn+1]  => -[m: Natm / succ: Nat → Natsucc n: Natn +1]
| -[_+1],  0: Int0       => 0: ?m.97350
| -[m: Natm+1],  succ: Nat → Natsucc n: Natn  => -[m: Natm / succ: Nat → Natsucc n: Natn +1]
| -[m: Natm+1],  -[n: Natn+1]  => ofNat: Nat → IntofNat (succ: Nat → Natsucc m: Natm / succ: Nat → Natsucc n: Natn)

/--
Integer modulus. This version of `Int.mod` uses the F-rounding convention
(flooring division), in which `Int.fdiv x y` satisfies `fdiv x y = floor (x / y)`
and `Int.fmod` is the unique function satisfying `fmod x y + (fdiv x y) * y = x`.
-/
def fmod: Int → Int → Intfmod : Int: TypeInt → Int: TypeInt → Int: TypeInt
| 0: Int0,       _       => 0: ?m.104240
| ofNat: Nat → IntofNat m: Natm, ofNat: Nat → IntofNat n: Natn => ofNat: Nat → IntofNat (m: Natm % n: Natn)
| succ: Nat → Natsucc m: Natm,  -[n: Natn+1]  => subNatNat: Nat → Nat → IntsubNatNat (m: Natm % succ: Nat → Natsucc n: Natn) n: Natn
| -[m: Natm+1],  ofNat: Nat → IntofNat n: Natn => subNatNat: Nat → Nat → IntsubNatNat n: Natn (succ: Nat → Natsucc (m: Natm % n: Natn))
| -[m: Natm+1],  -[n: Natn+1]  => -ofNat: Nat → IntofNat (succ: Nat → Natsucc m: Natm % succ: Nat → Natsucc n: Natn)

/-! ### T-rounding division

This pair satisfies `div x y = round_to_zero (x / y)`.
`Int.div` and `Int.mod` are defined in core lean.
-/

/--
Core Lean provides instances using T-rounding division, i.e. `Int.div` and `Int.mod`.
We override these here.
-/
instance: Div Intinstance : Div: Type ?u.11189 → Type ?u.11189Div Int: TypeInt := ⟨Int.ediv: Int → Int → IntInt.ediv⟩
instance: Mod Intinstance : Mod: Type ?u.11219 → Type ?u.11219Mod Int: TypeInt := ⟨Int.emod: Int → Int → IntInt.emod⟩

/-! ## gcd -/

/-- Computes the greatest common divisor of two integers, as a `Nat`. -/
def gcd: Int → Int → Natgcd (m: Intm n: Intn : Int: TypeInt) : Nat: TypeNat := m: Intm.natAbs: Int → NatnatAbs.gcd: Nat → Nat → Natgcd n: Intn.natAbs: Int → NatnatAbs

/-! ## divisibility -/

/--
Divisibility of integers. `a ∣ b` (typed as `\|`) says that
there is some `c` such that `b = a * c`.
-/
instance: Dvd Intinstance : Dvd: Type ?u.11282 → Type ?u.11282Dvd Int: TypeInt := ⟨fun a: ?m.11290a b: ?m.11293b => ∃ c: ?m.11298c, b: ?m.11293b = a: ?m.11290a * c: ?m.11298c⟩
```