/-
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad
-/

import Mathlib.Init.Algebra.Order
import Mathlib.Init.Data.Int.Basic

/-! # The order relation on the integers -/

open Nat

namespace Int

#align int.nonneg Int.NonNeg: ℤ → Prop
Int.NonNeg
#align int.le Int.le: ℤ → ℤ → Prop
Int.le
#align int.lt Int.lt: ℤ → ℤ → Prop
Int.lt

export private decNonneg: (m : ℤ) → Decidable (NonNeg m)
decNonneg from Init.Data.Int.Basic
#align int.decidable_nonneg Int.decNonneg: (m : ℤ) → Decidable (NonNeg m)
Int.decNonneg
#align int.decidable_le Int.decLe: (a b : ℤ) → Decidable (a ≤ b)
Int.decLe
#align int.decidable_lt Int.decLt: (a b : ℤ) → Decidable (a < b)
Int.decLt

theorem le.elim: ∀ {a b : ℤ}, a ≤ b → ∀ {P : Prop}, (∀ (n : ℕ), a + ↑n = b → P) → P
le.elim {a: ℤ
a b: ℤ
b : ℤ: Type
ℤ} (h: a ≤ b
h : a: ℤ
a ≤ b: ℤ
b) {P: Prop
P : Prop: Type
Prop} (h': ∀ (n : ℕ), a + ↑n = b → P
h' : ∀ n: ℕ
n : ℕ: Type
ℕ, a: ℤ
a + ↑n: ℕ
n = b: ℤ
b → P: Prop
P) : P: Prop
P :=
  Exists.elim: ∀ {α : Sort ?u.111} {p : α → Prop} {b : Prop}, (∃ x, p x) → (∀ (a : α), p a → b) → b
Exists.elim (le.dest: ∀ {a b : ℤ}, a ≤ b → ∃ n, a + ↑n = b
le.dest h: a ≤ b
h) h': ∀ (n : ℕ), a + ↑n = b → P
h'
#align int.le.elim Int.le.elim: ∀ {a b : ℤ}, a ≤ b → ∀ {P : Prop}, (∀ (n : ℕ), a + ↑n = b → P) → P
Int.le.elim

alias ofNat_le: ∀ {m n : ℕ}, ↑m ≤ ↑n ↔ m ≤ n
ofNat_le ↔ le_of_ofNat_le_ofNat: ∀ {m n : ℕ}, ↑m ≤ ↑n → m ≤ n
le_of_ofNat_le_ofNat ofNat_le_ofNat_of_le: ∀ {m n : ℕ}, m ≤ n → ↑m ≤ ↑n
ofNat_le_ofNat_of_le
#align int.coe_nat_le_coe_nat_of_le Int.ofNat_le_ofNat_of_le: ∀ {m n : ℕ}, m ≤ n → ↑m ≤ ↑n
Int.ofNat_le_ofNat_of_le
#align int.le_of_coe_nat_le_coe_nat Int.le_of_ofNat_le_ofNat: ∀ {m n : ℕ}, ↑m ≤ ↑n → m ≤ n
Int.le_of_ofNat_le_ofNat
#align int.coe_nat_le_coe_nat_iff Int.ofNat_le: ∀ {m n : ℕ}, ↑m ≤ ↑n ↔ m ≤ n
Int.ofNat_le

#align int.coe_zero_le Int.ofNat_zero_le: ∀ (n : ℕ), 0 ≤ ↑n
Int.ofNat_zero_le
#align int.eq_coe_of_zero_le Int.eq_ofNat_of_zero_le: ∀ {a : ℤ}, 0 ≤ a → ∃ n, a = ↑n
Int.eq_ofNat_of_zero_le

theorem lt.elim: ∀ {a b : ℤ}, a < b → ∀ {P : Prop}, (∀ (n : ℕ), a + ↑(succ n) = b → P) → P
lt.elim {a: ℤ
a b: ℤ
b : ℤ: Type
ℤ} (h: a < b
h : a: ℤ
a < b: ℤ
b) {P: Prop
P : Prop: Type
Prop} (h': ∀ (n : ℕ), a + ↑(succ n) = b → P
h' : ∀ n: ℕ
n : ℕ: Type
ℕ, a: ℤ
a + ↑(Nat.succ: ℕ → ℕ
Nat.succ n: ℕ
n) = b: ℤ
b → P: Prop
P) : P: Prop
P :=
  Exists.elim: ∀ {α : Sort ?u.253} {p : α → Prop} {b : Prop}, (∃ x, p x) → (∀ (a : α), p a → b) → b
Exists.elim (lt.dest: ∀ {a b : ℤ}, a < b → ∃ n, a + ↑(succ n) = b
lt.dest h: a < b
h) h': ∀ (n : ℕ), a + ↑(succ n) = b → P
h'
#align int.lt.elim Int.lt.elim: ∀ {a b : ℤ}, a < b → ∀ {P : Prop}, (∀ (n : ℕ), a + ↑(succ n) = b → P) → P
Int.lt.elim

alias ofNat_lt: ∀ {n m : ℕ}, ↑n < ↑m ↔ n < m
ofNat_lt ↔ lt_of_ofNat_lt_ofNat: ∀ {n m : ℕ}, ↑n < ↑m → n < m
lt_of_ofNat_lt_ofNat ofNat_lt_ofNat_of_lt: ∀ {n m : ℕ}, n < m → ↑n < ↑m
ofNat_lt_ofNat_of_lt
#align int.coe_nat_lt_coe_nat_iff Int.ofNat_lt: ∀ {n m : ℕ}, ↑n < ↑m ↔ n < m
Int.ofNat_lt
#align int.lt_of_coe_nat_lt_coe_nat Int.lt_of_ofNat_lt_ofNat: ∀ {n m : ℕ}, ↑n < ↑m → n < m
Int.lt_of_ofNat_lt_ofNat
#align int.coe_nat_lt_coe_nat_of_lt Int.ofNat_lt_ofNat_of_lt: ∀ {n m : ℕ}, n < m → ↑n < ↑m
Int.ofNat_lt_ofNat_of_lt

instance: LinearOrder ℤ
instance : LinearOrder: Type ?u.295 → Type ?u.295
LinearOrder ℤ: Type
ℤ where
  le := (·≤·): ℤ → ℤ → Prop
(·≤·)
  le_refl := Int.le_refl: ∀ (a : ℤ), a ≤ a
Int.le_refl
  le_trans := @Int.le_trans: ∀ {a b c : ℤ}, a ≤ b → b ≤ c → a ≤ c
Int.le_trans
  le_antisymm := @Int.le_antisymm: ∀ {a b : ℤ}, a ≤ b → b ≤ a → a = b
Int.le_antisymm
  lt := (·<·): ℤ → ℤ → Prop
(·<·)
  lt_iff_le_not_le := @Int.lt_iff_le_not_le: ∀ {a b : ℤ}, a < b ↔ a ≤ b ∧ ¬b ≤ a
Int.lt_iff_le_not_le
  le_total := Int.le_total: ∀ (a b : ℤ), a ≤ b ∨ b ≤ a
Int.le_total
  decidableEq := by
Goals accomplished! 🐙 
DecidableEq ℤinfer_instance
Goals accomplished! 🐙
  decidableLE := by
Goals accomplished! 🐙 
DecidableRel fun x x_1 => x ≤ x_1infer_instance
Goals accomplished! 🐙
  decidableLT := by
Goals accomplished! 🐙 
DecidableRel fun x x_1 => x < x_1infer_instance
Goals accomplished! 🐙

#align int.eq_nat_abs_of_zero_le Int.eq_natAbs_of_zero_le: ∀ {a : ℤ}, 0 ≤ a → a = ↑(natAbs a)
Int.eq_natAbs_of_zero_le
#align int.le_nat_abs Int.le_natAbs: ∀ {a : ℤ}, a ≤ ↑(natAbs a)
Int.le_natAbs
#align int.neg_succ_lt_zero Int.negSucc_lt_zero: ∀ (n : ℕ), -[n+1] < 0
Int.negSucc_lt_zero
#align int.eq_neg_succ_of_lt_zero Int.eq_negSucc_of_lt_zero: ∀ {a : ℤ}, a < 0 → ∃ n, a = -[n+1]
Int.eq_negSucc_of_lt_zero
#align int.sub_eq_zero_iff_eq Int.sub_eq_zero: ∀ {a b : ℤ}, a - b = 0 ↔ a = b
Int.sub_eq_zero

theorem neg_mul_eq_neg_mul_symm: ∀ (a b : ℤ), -a * b = -(a * b)
neg_mul_eq_neg_mul_symm (a: ℤ
a b: ℤ
b : ℤ: Type
ℤ) : -a: ℤ
a * b: ℤ
b = -(a: ℤ
a * b: ℤ
b) := (Int.neg_mul_eq_neg_mul: ∀ (a b : ℤ), -(a * b) = -a * b
Int.neg_mul_eq_neg_mul a: ℤ
a b: ℤ
b).symm: ∀ {α : Sort ?u.1054} {a b : α}, a = b → b = a
symm
#align int.neg_mul_eq_neg_mul_symm Int.neg_mul_eq_neg_mul_symm: ∀ (a b : ℤ), -a * b = -(a * b)
Int.neg_mul_eq_neg_mul_symm

theorem mul_neg_eq_neg_mul_symm: ∀ (a b : ℤ), a * -b = -(a * b)
mul_neg_eq_neg_mul_symm (a: ℤ
a b: ℤ
b : ℤ: Type
ℤ) : a: ℤ
a * -b: ℤ
b = -(a: ℤ
a * b: ℤ
b) := (Int.neg_mul_eq_mul_neg: ∀ (a b : ℤ), -(a * b) = a * -b
Int.neg_mul_eq_mul_neg a: ℤ
a b: ℤ
b).symm: ∀ {α : Sort ?u.1140} {a b : α}, a = b → b = a
symm
#align int.mul_neg_eq_neg_mul_symm Int.mul_neg_eq_neg_mul_symm: ∀ (a b : ℤ), a * -b = -(a * b)
Int.mul_neg_eq_neg_mul_symm

#align int.of_nat_nonneg Int.ofNat_nonneg: ∀ (n : ℕ), 0 ≤ ↑n
Int.ofNat_nonneg
#align int.coe_succ_pos Int.ofNat_succ_pos: ∀ (n : ℕ), 0 < ↑(succ n)
Int.ofNat_succ_pos
#align int.exists_eq_neg_of_nat Int.exists_eq_neg_ofNat: ∀ {a : ℤ}, a ≤ 0 → ∃ n, a = -↑n
Int.exists_eq_neg_ofNat
#align int.nat_abs_of_nonneg Int.natAbs_of_nonneg: ∀ {a : ℤ}, 0 ≤ a → ↑(natAbs a) = a
Int.natAbs_of_nonneg
#align int.of_nat_nat_abs_of_nonpos Int.ofNat_natAbs_of_nonpos: ∀ {a : ℤ}, a ≤ 0 → ↑(natAbs a) = -a
Int.ofNat_natAbs_of_nonpos

protected theorem eq_zero_or_eq_zero_of_mul_eq_zero: ∀ {a b : ℤ}, a * b = 0 → a = 0 ∨ b = 0
eq_zero_or_eq_zero_of_mul_eq_zero {a: ℤ
a b: ℤ
b : ℤ: Type
ℤ} (h: a * b = 0
h : a: ℤ
a * b: ℤ
b = 0: ?m.1163
0) : a: ℤ
a = 0: ?m.1219
0 ∨ b: ℤ
b = 0: ?m.1235
0 :=
  match lt_trichotomy: ∀ {α : Type ?u.1253} [inst : LinearOrder α] (a b : α), a < b ∨ a = b ∨ b < a
lt_trichotomy 0: ?m.1257
0 a: ℤ
a with
  | Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl hlt₁: 0 < a
hlt₁ =>
    match lt_trichotomy: ∀ {α : Type ?u.1286} [inst : LinearOrder α] (a b : α), a < b ∨ a = b ∨ b < a
lt_trichotomy 0: ?m.1290
0 b: ℤ
b with
    | Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl hlt₂: 0 < b
hlt₂ => by
Goals accomplished! 🐙
      a, b: ℤ

h: a * b = 0

hlt₁: 0 < a

hlt₂: 0 < b

a = 0 ∨ b = 0have : 0: ?m.1818
0 < a: ℤ
a * b: ℤ
b := Int.mul_pos: ∀ {a b : ℤ}, 0 < a → 0 < b → 0 < a * b
Int.mul_pos hlt₁: 0 < a
hlt₁ hlt₂: 0 < b
hlt₂a, b: ℤ

h: a * b = 0

hlt₁: 0 < a

hlt₂: 0 < b

this: 0 < a * b

a = 0 ∨ b = 0
      a, b: ℤ

h: a * b = 0

hlt₁: 0 < a

hlt₂: 0 < b

a = 0 ∨ b = 0rw [a, b: ℤ

h: a * b = 0

hlt₁: 0 < a

hlt₂: 0 < b

this: 0 < a * b

a = 0 ∨ b = 0h: a * b = 0
ha, b: ℤ

h: a * b = 0

hlt₁: 0 < a

hlt₂: 0 < b

this: 0 < 0

a = 0 ∨ b = 0]a, b: ℤ

h: a * b = 0

hlt₁: 0 < a

hlt₂: 0 < b

this: 0 < 0

a = 0 ∨ b = 0 at this: 0 < a * b
thisa, b: ℤ

h: a * b = 0

hlt₁: 0 < a

hlt₂: 0 < b

this: 0 < 0

a = 0 ∨ b = 0
      a, b: ℤ

h: a * b = 0

hlt₁: 0 < a

hlt₂: 0 < b

a = 0 ∨ b = 0exact absurd: ∀ {a : Prop} {b : Sort ?u.1907}, a → ¬a → b
absurd this: 0 < 0
this (lt_irrefl: ∀ {α : Type ?u.1910} [inst : Preorder α] (a : α), ¬a < a
lt_irrefl _: ?m.1911
_)
Goals accomplished! 🐙
    | Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr (Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl heq₂: 0 = b
heq₂) => Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr heq₂: 0 = b
heq₂.symm: ∀ {α : Sort ?u.1338} {a b : α}, a = b → b = a
symm
    | Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr (Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr hgt₂: b < 0
hgt₂) => by
Goals accomplished! 🐙
      a, b: ℤ

h: a * b = 0

hlt₁: 0 < a

hgt₂: b < 0

a = 0 ∨ b = 0have : 0: ?m.1947
0 > a: ℤ
a * b: ℤ
b := Int.mul_neg_of_pos_of_neg: ∀ {a b : ℤ}, 0 < a → b < 0 → a * b < 0
Int.mul_neg_of_pos_of_neg hlt₁: 0 < a
hlt₁ hgt₂: b < 0
hgt₂a, b: ℤ

h: a * b = 0

hlt₁: 0 < a

hgt₂: b < 0

this: 0 > a * b

a = 0 ∨ b = 0
      a, b: ℤ

h: a * b = 0

hlt₁: 0 < a

hgt₂: b < 0

a = 0 ∨ b = 0rw [a, b: ℤ

h: a * b = 0

hlt₁: 0 < a

hgt₂: b < 0

this: 0 > a * b

a = 0 ∨ b = 0h: a * b = 0
ha, b: ℤ

h: a * b = 0

hlt₁: 0 < a

hgt₂: b < 0

this: 0 > 0

a = 0 ∨ b = 0]a, b: ℤ

h: a * b = 0

hlt₁: 0 < a

hgt₂: b < 0

this: 0 > 0

a = 0 ∨ b = 0 at this: 0 > a * b
thisa, b: ℤ

h: a * b = 0

hlt₁: 0 < a

hgt₂: b < 0

this: 0 > 0

a = 0 ∨ b = 0
      a, b: ℤ

h: a * b = 0

hlt₁: 0 < a

hgt₂: b < 0

a = 0 ∨ b = 0exact absurd: ∀ {a : Prop} {b : Sort ?u.2014}, a → ¬a → b
absurd this: 0 > 0
this (lt_irrefl: ∀ {α : Type ?u.2017} [inst : Preorder α] (a : α), ¬a < a
lt_irrefl _: ?m.2018
_)
Goals accomplished! 🐙
  | Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr (Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl heq₁: 0 = a
heq₁) => Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl heq₁: 0 = a
heq₁.symm: ∀ {α : Sort ?u.1502} {a b : α}, a = b → b = a
symm
  | Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr (Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr hgt₁: a < 0
hgt₁) =>
    match lt_trichotomy: ∀ {α : Type ?u.1532} [inst : LinearOrder α] (a b : α), a < b ∨ a = b ∨ b < a
lt_trichotomy 0: ?m.1536
0 b: ℤ
b with
    | Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl hlt₂: 0 < b
hlt₂ => by
Goals accomplished! 🐙
      a, b: ℤ

h: a * b = 0

hgt₁: a < 0

hlt₂: 0 < b

a = 0 ∨ b = 0have : 0: ?m.2038
0 > a: ℤ
a * b: ℤ
b := Int.mul_neg_of_neg_of_pos: ∀ {a b : ℤ}, a < 0 → 0 < b → a * b < 0
Int.mul_neg_of_neg_of_pos hgt₁: a < 0
hgt₁ hlt₂: 0 < b
hlt₂a, b: ℤ

h: a * b = 0

hgt₁: a < 0

hlt₂: 0 < b

this: 0 > a * b

a = 0 ∨ b = 0
      a, b: ℤ

h: a * b = 0

hgt₁: a < 0

hlt₂: 0 < b

a = 0 ∨ b = 0rw [a, b: ℤ

h: a * b = 0

hgt₁: a < 0

hlt₂: 0 < b

this: 0 > a * b

a = 0 ∨ b = 0h: a * b = 0
ha, b: ℤ

h: a * b = 0

hgt₁: a < 0

hlt₂: 0 < b

this: 0 > 0

a = 0 ∨ b = 0]a, b: ℤ

h: a * b = 0

hgt₁: a < 0

hlt₂: 0 < b

this: 0 > 0

a = 0 ∨ b = 0 at this: 0 > a * b
thisa, b: ℤ

h: a * b = 0

hgt₁: a < 0

hlt₂: 0 < b

this: 0 > 0

a = 0 ∨ b = 0
      a, b: ℤ

h: a * b = 0

hgt₁: a < 0

hlt₂: 0 < b

a = 0 ∨ b = 0exact absurd: ∀ {a : Prop} {b : Sort ?u.2100}, a → ¬a → b
absurd this: 0 > 0
this (lt_irrefl: ∀ {α : Type ?u.2103} [inst : Preorder α] (a : α), ¬a < a
lt_irrefl _: ?m.2104
_)
Goals accomplished! 🐙
    | Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr (Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl heq₂: 0 = b
heq₂) => Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr heq₂: 0 = b
heq₂.symm: ∀ {α : Sort ?u.1586} {a b : α}, a = b → b = a
symm
    | Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr (Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr hgt₂: b < 0
hgt₂) => by
Goals accomplished! 🐙
      a, b: ℤ

h: a * b = 0

hgt₁: a < 0

hgt₂: b < 0

a = 0 ∨ b = 0have : 0: ?m.2124
0 < a: ℤ
a * b: ℤ
b := Int.mul_pos_of_neg_of_neg: ∀ {a b : ℤ}, a < 0 → b < 0 → 0 < a * b
Int.mul_pos_of_neg_of_neg hgt₁: a < 0
hgt₁ hgt₂: b < 0
hgt₂a, b: ℤ

h: a * b = 0

hgt₁: a < 0

hgt₂: b < 0

this: 0 < a * b

a = 0 ∨ b = 0
      a, b: ℤ

h: a * b = 0

hgt₁: a < 0

hgt₂: b < 0

a = 0 ∨ b = 0rw [a, b: ℤ

h: a * b = 0

hgt₁: a < 0

hgt₂: b < 0

this: 0 < a * b

a = 0 ∨ b = 0h: a * b = 0
ha, b: ℤ

h: a * b = 0

hgt₁: a < 0

hgt₂: b < 0

this: 0 < 0

a = 0 ∨ b = 0]a, b: ℤ

h: a * b = 0

hgt₁: a < 0

hgt₂: b < 0

this: 0 < 0

a = 0 ∨ b = 0 at this: 0 < a * b
thisa, b: ℤ

h: a * b = 0

hgt₁: a < 0

hgt₂: b < 0

this: 0 < 0

a = 0 ∨ b = 0
      a, b: ℤ

h: a * b = 0

hgt₁: a < 0

hgt₂: b < 0

a = 0 ∨ b = 0exact absurd: ∀ {a : Prop} {b : Sort ?u.2186}, a → ¬a → b
absurd this: 0 < 0
this (lt_irrefl: ∀ {α : Type ?u.2189} [inst : Preorder α] (a : α), ¬a < a
lt_irrefl _: ?m.2190
_)
Goals accomplished! 🐙
#align int.eq_zero_or_eq_zero_of_mul_eq_zero Int.eq_zero_or_eq_zero_of_mul_eq_zero: ∀ {a b : ℤ}, a * b = 0 → a = 0 ∨ b = 0
Int.eq_zero_or_eq_zero_of_mul_eq_zero