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

! This file was ported from Lean 3 source module data.int.lemmas
! leanprover-community/mathlib commit 09597669f02422ed388036273d8848119699c22f
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Set.Function
import Mathlib.Data.Int.Order.Lemmas
import Mathlib.Data.Int.Bitwise
import Mathlib.Data.Nat.Cast.Basic
import Mathlib.Data.Nat.Order.Lemmas

/-!
# Miscellaneous lemmas about the integers

This file contains lemmas about integers, which require further imports than
`Data.Int.Basic` or `Data.Int.Order`.

-/


open Nat

namespace Int

theorem 
le_coe_nat_sub: ∀ (m n : ℕ), ↑m - ↑n ≤ ↑(m - n)
le_coe_nat_sub (
m: ℕ
m 
n: ℕ
n : 
ℕ: Type
ℕ) : (
m: ℕ
m - 
n: ℕ
n : 
ℤ: Type
ℤ) ≤ ↑(
m: ℕ
m - 
n: ℕ
n : 
ℕ: Type
ℕ) := by
Goals accomplished! 🐙
  
m, n: ℕ

↑m - ↑n ≤ ↑(m - n)by_cases 
h: ?m.288
h : 
m: ℕ
m ≥ 
n: ℕ
n
m, n: ℕ

h: m ≥ n

pos
↑m - ↑n ≤ ↑(m - n)
m, n: ℕ

h: ¬m ≥ n

neg
↑m - ↑n ≤ ↑(m - n)
  
m, n: ℕ

↑m - ↑n ≤ ↑(m - n)·
m, n: ℕ

h: m ≥ n

pos
↑m - ↑n ≤ ↑(m - n) 
m, n: ℕ

h: m ≥ n

pos
↑m - ↑n ≤ ↑(m - n)
m, n: ℕ

h: ¬m ≥ n

neg
↑m - ↑n ≤ ↑(m - n)exact 
le_of_eq: ∀ {α : Type ?u.302} [inst : Preorder α] {a b : α}, a = b → a ≤ b
le_of_eq (
Int.ofNat_sub: ∀ {m n : ℕ}, m ≤ n → ↑(n - m) = ↑n - ↑m
Int.ofNat_sub 
h: ?m.288
h).
symm: ∀ {α : Sort ?u.374} {a b : α}, a = b → b = a
symm
Goals accomplished! 🐙
  
m, n: ℕ

↑m - ↑n ≤ ↑(m - n)·
m, n: ℕ

h: ¬m ≥ n

neg
↑m - ↑n ≤ ↑(m - n) 
m, n: ℕ

h: ¬m ≥ n

neg
↑m - ↑n ≤ ↑(m - n)simp [
le_of_not_ge: ∀ {α : Type ?u.386} [inst : LinearOrder α] {a b : α}, ¬a ≥ b → a ≤ b
le_of_not_ge 
h: ?m.295
h, 
ofNat_le: ∀ {m n : ℕ}, ↑m ≤ ↑n ↔ m ≤ n
ofNat_le]
Goals accomplished! 🐙
#align int.le_coe_nat_sub 
Int.le_coe_nat_sub: ∀ (m n : ℕ), ↑m - ↑n ≤ ↑(m - n)
Int.le_coe_nat_sub

/-! ### `succ` and `pred` -/


-- Porting note: simp can prove this @[simp]
theorem 
succ_coe_nat_pos: ∀ (n : ℕ), 0 < ↑n + 1
succ_coe_nat_pos (
n: ℕ
n : 
ℕ: Type
ℕ) : 
0: ?m.1564
0 < (
n: ℕ
n : 
ℤ: Type
ℤ) + 
1: ?m.1624
1 :=
  
lt_add_one_iff: ∀ {a b : ℤ}, a < b + 1 ↔ a ≤ b
lt_add_one_iff.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr (by
Goals accomplished! 🐙 
n: ℕ

0 ≤ ↑nsimp
Goals accomplished! 🐙)
#align int.succ_coe_nat_pos 
Int.succ_coe_nat_pos: ∀ (n : ℕ), 0 < ↑n + 1
Int.succ_coe_nat_pos

/-! ### `natAbs` -/


variable {
a: ℤ
a 
b: ℤ
b : 
ℤ: Type
ℤ} {
n: ℕ
n : 
ℕ: Type
ℕ}

theorem 
natAbs_eq_iff_sq_eq: ∀ {a b : ℤ}, natAbs a = natAbs b ↔ a ^ 2 = b ^ 2
natAbs_eq_iff_sq_eq {
a: ℤ
a 
b: ℤ
b : 
ℤ: Type
ℤ} : 
a: ℤ
a.
natAbs: ℤ → ℕ
natAbs = 
b: ℤ
b.
natAbs: ℤ → ℕ
natAbs ↔ 
a: ℤ
a ^ 
2: ?m.1981
2 = 
b: ℤ
b ^ 
2: ?m.1998
2 := by
Goals accomplished! 🐙
  
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a = natAbs b ↔ a ^ 2 = b ^ 2rw [
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a = natAbs b ↔ a ^ 2 = b ^ 2
sq: ∀ {M : Type ?u.2278} [inst : Monoid M] (a : M), a ^ 2 = a * a
sq,
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a = natAbs b ↔ a * a = b ^ 2 
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a = natAbs b ↔ a ^ 2 = b ^ 2
sq: ∀ {M : Type ?u.2334} [inst : Monoid M] (a : M), a ^ 2 = a * a
sq
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a = natAbs b ↔ a * a = b * b]
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a = natAbs b ↔ a * a = b * b
  
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a = natAbs b ↔ a ^ 2 = b ^ 2exact 
natAbs_eq_iff_mul_self_eq: ∀ {a b : ℤ}, natAbs a = natAbs b ↔ a * a = b * b
natAbs_eq_iff_mul_self_eq
Goals accomplished! 🐙
#align int.nat_abs_eq_iff_sq_eq 
Int.natAbs_eq_iff_sq_eq: ∀ {a b : ℤ}, natAbs a = natAbs b ↔ a ^ 2 = b ^ 2
Int.natAbs_eq_iff_sq_eq

theorem 
natAbs_lt_iff_sq_lt: ∀ {a b : ℤ}, natAbs a < natAbs b ↔ a ^ 2 < b ^ 2
natAbs_lt_iff_sq_lt {
a: ℤ
a 
b: ℤ
b : 
ℤ: Type
ℤ} : 
a: ℤ
a.
natAbs: ℤ → ℕ
natAbs < 
b: ℤ
b.
natAbs: ℤ → ℕ
natAbs ↔ 
a: ℤ
a ^ 
2: ?m.2435
2 < 
b: ℤ
b ^ 
2: ?m.2452
2 := by
Goals accomplished! 🐙
  
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a < natAbs b ↔ a ^ 2 < b ^ 2rw [
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a < natAbs b ↔ a ^ 2 < b ^ 2
sq: ∀ {M : Type ?u.2787} [inst : Monoid M] (a : M), a ^ 2 = a * a
sq,
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a < natAbs b ↔ a * a < b ^ 2 
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a < natAbs b ↔ a ^ 2 < b ^ 2
sq: ∀ {M : Type ?u.2843} [inst : Monoid M] (a : M), a ^ 2 = a * a
sq
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a < natAbs b ↔ a * a < b * b]
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a < natAbs b ↔ a * a < b * b
  
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a < natAbs b ↔ a ^ 2 < b ^ 2exact 
natAbs_lt_iff_mul_self_lt: ∀ {a b : ℤ}, natAbs a < natAbs b ↔ a * a < b * b
natAbs_lt_iff_mul_self_lt
Goals accomplished! 🐙
#align int.nat_abs_lt_iff_sq_lt 
Int.natAbs_lt_iff_sq_lt: ∀ {a b : ℤ}, natAbs a < natAbs b ↔ a ^ 2 < b ^ 2
Int.natAbs_lt_iff_sq_lt

theorem 
natAbs_le_iff_sq_le: ∀ {a b : ℤ}, natAbs a ≤ natAbs b ↔ a ^ 2 ≤ b ^ 2
natAbs_le_iff_sq_le {
a: ℤ
a 
b: ℤ
b : 
ℤ: Type
ℤ} : 
a: ℤ
a.
natAbs: ℤ → ℕ
natAbs ≤ 
b: ℤ
b.
natAbs: ℤ → ℕ
natAbs ↔ 
a: ℤ
a ^ 
2: ?m.2948
2 ≤ 
b: ℤ
b ^ 
2: ?m.2965
2 := by
Goals accomplished! 🐙
  
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a ≤ natAbs b ↔ a ^ 2 ≤ b ^ 2rw [
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a ≤ natAbs b ↔ a ^ 2 ≤ b ^ 2
sq: ∀ {M : Type ?u.3312} [inst : Monoid M] (a : M), a ^ 2 = a * a
sq,
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a ≤ natAbs b ↔ a * a ≤ b ^ 2 
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a ≤ natAbs b ↔ a ^ 2 ≤ b ^ 2
sq: ∀ {M : Type ?u.3368} [inst : Monoid M] (a : M), a ^ 2 = a * a
sq
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a ≤ natAbs b ↔ a * a ≤ b * b]
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a ≤ natAbs b ↔ a * a ≤ b * b
  
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

natAbs a ≤ natAbs b ↔ a ^ 2 ≤ b ^ 2exact 
natAbs_le_iff_mul_self_le: ∀ {a b : ℤ}, natAbs a ≤ natAbs b ↔ a * a ≤ b * b
natAbs_le_iff_mul_self_le
Goals accomplished! 🐙
#align int.nat_abs_le_iff_sq_le 
Int.natAbs_le_iff_sq_le: ∀ {a b : ℤ}, natAbs a ≤ natAbs b ↔ a ^ 2 ≤ b ^ 2
Int.natAbs_le_iff_sq_le

theorem 
natAbs_inj_of_nonneg_of_nonneg: ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → (natAbs a = natAbs b ↔ a = b)
natAbs_inj_of_nonneg_of_nonneg {
a: ℤ
a 
b: ℤ
b : 
ℤ: Type
ℤ} (
ha: 0 ≤ a
ha : 
0: ?m.3462
0 ≤ 
a: ℤ
a) (
hb: 0 ≤ b
hb : 
0: ?m.3499
0 ≤ 
b: ℤ
b) :
    
natAbs: ℤ → ℕ
natAbs 
a: ℤ
a = 
natAbs: ℤ → ℕ
natAbs 
b: ℤ
b ↔ 
a: ℤ
a = 
b: ℤ
b := by
Goals accomplished! 🐙 
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

ha: 0 ≤ a

hb: 0 ≤ b

natAbs a = natAbs b ↔ a = brw [
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

ha: 0 ≤ a

hb: 0 ≤ b

natAbs a = natAbs b ↔ a = b← 
sq_eq_sq: ∀ {R : Type ?u.3534} [inst : LinearOrderedSemiring R] {a b : R}, 0 ≤ a → 0 ≤ b → (a ^ 2 = b ^ 2 ↔ a = b)
sq_eq_sq 
ha: 0 ≤ a
ha 
hb: 0 ≤ b
hb,
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

ha: 0 ≤ a

hb: 0 ≤ b

natAbs a = natAbs b ↔ a ^ 2 = b ^ 2 
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

ha: 0 ≤ a

hb: 0 ≤ b

natAbs a = natAbs b ↔ a = b← 
natAbs_eq_iff_sq_eq: ∀ {a b : ℤ}, natAbs a = natAbs b ↔ a ^ 2 = b ^ 2
natAbs_eq_iff_sq_eq
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

ha: 0 ≤ a

hb: 0 ≤ b

natAbs a = natAbs b ↔ natAbs a = natAbs b]
Goals accomplished! 🐙
#align int.nat_abs_inj_of_nonneg_of_nonneg 
Int.natAbs_inj_of_nonneg_of_nonneg: ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → (natAbs a = natAbs b ↔ a = b)
Int.natAbs_inj_of_nonneg_of_nonneg

theorem 
natAbs_inj_of_nonpos_of_nonpos: ∀ {a b : ℤ}, a ≤ 0 → b ≤ 0 → (natAbs a = natAbs b ↔ a = b)
natAbs_inj_of_nonpos_of_nonpos {
a: ℤ
a 
b: ℤ
b : 
ℤ: Type
ℤ} (
ha: a ≤ 0
ha : 
a: ℤ
a ≤ 
0: ?m.3661
0) (
hb: b ≤ 0
hb : 
b: ℤ
b ≤ 
0: ?m.3693
0) :
    
natAbs: ℤ → ℕ
natAbs 
a: ℤ
a = 
natAbs: ℤ → ℕ
natAbs 
b: ℤ
b ↔ 
a: ℤ
a = 
b: ℤ
b := by
Goals accomplished! 🐙
  
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

ha: a ≤ 0

hb: b ≤ 0

natAbs a = natAbs b ↔ a = bsimpa only [
Int.natAbs_neg: ∀ (a : ℤ), natAbs (-a) = natAbs a
Int.natAbs_neg, 
neg_inj: ∀ {G : Type ?u.3741} [inst : InvolutiveNeg G] {a b : G}, -a = -b ↔ a = b
neg_inj] using
    
natAbs_inj_of_nonneg_of_nonneg: ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → (natAbs a = natAbs b ↔ a = b)
natAbs_inj_of_nonneg_of_nonneg (
neg_nonneg_of_nonpos: ∀ {α : Type ?u.3796} [inst : OrderedAddCommGroup α] {a : α}, a ≤ 0 → 0 ≤ -a
neg_nonneg_of_nonpos 
ha: a ≤ 0
ha) (
neg_nonneg_of_nonpos: ∀ {α : Type ?u.3855} [inst : OrderedAddCommGroup α] {a : α}, a ≤ 0 → 0 ≤ -a
neg_nonneg_of_nonpos 
hb: b ≤ 0
hb)
Goals accomplished! 🐙
#align int.nat_abs_inj_of_nonpos_of_nonpos 
Int.natAbs_inj_of_nonpos_of_nonpos: ∀ {a b : ℤ}, a ≤ 0 → b ≤ 0 → (natAbs a = natAbs b ↔ a = b)
Int.natAbs_inj_of_nonpos_of_nonpos

theorem 
natAbs_inj_of_nonneg_of_nonpos: ∀ {a b : ℤ}, 0 ≤ a → b ≤ 0 → (natAbs a = natAbs b ↔ a = -b)
natAbs_inj_of_nonneg_of_nonpos {
a: ℤ
a 
b: ℤ
b : 
ℤ: Type
ℤ} (
ha: 0 ≤ a
ha : 
0: ?m.4076
0 ≤ 
a: ℤ
a) (
hb: b ≤ 0
hb : 
b: ℤ
b ≤ 
0: ?m.4113
0) :
    
natAbs: ℤ → ℕ
natAbs 
a: ℤ
a = 
natAbs: ℤ → ℕ
natAbs 
b: ℤ
b ↔ 
a: ℤ
a = -
b: ℤ
b := by
Goals accomplished! 🐙
  
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

ha: 0 ≤ a

hb: b ≤ 0

natAbs a = natAbs b ↔ a = -bsimpa only [
Int.natAbs_neg: ∀ (a : ℤ), natAbs (-a) = natAbs a
Int.natAbs_neg] using 
natAbs_inj_of_nonneg_of_nonneg: ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → (natAbs a = natAbs b ↔ a = b)
natAbs_inj_of_nonneg_of_nonneg 
ha: 0 ≤ a
ha (
neg_nonneg_of_nonpos: ∀ {α : Type ?u.4212} [inst : OrderedAddCommGroup α] {a : α}, a ≤ 0 → 0 ≤ -a
neg_nonneg_of_nonpos 
hb: b ≤ 0
hb)
Goals accomplished! 🐙
#align int.nat_abs_inj_of_nonneg_of_nonpos 
Int.natAbs_inj_of_nonneg_of_nonpos: ∀ {a b : ℤ}, 0 ≤ a → b ≤ 0 → (natAbs a = natAbs b ↔ a = -b)
Int.natAbs_inj_of_nonneg_of_nonpos

theorem 
natAbs_inj_of_nonpos_of_nonneg: ∀ {a b : ℤ}, a ≤ 0 → 0 ≤ b → (natAbs a = natAbs b ↔ -a = b)
natAbs_inj_of_nonpos_of_nonneg {
a: ℤ
a 
b: ℤ
b : 
ℤ: Type
ℤ} (
ha: a ≤ 0
ha : 
a: ℤ
a ≤ 
0: ?m.4391
0) (
hb: 0 ≤ b
hb : 
0: ?m.4423
0 ≤ 
b: ℤ
b) :
    
natAbs: ℤ → ℕ
natAbs 
a: ℤ
a = 
natAbs: ℤ → ℕ
natAbs 
b: ℤ
b ↔ -
a: ℤ
a = 
b: ℤ
b := by
Goals accomplished! 🐙
  
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

ha: a ≤ 0

hb: 0 ≤ b

natAbs a = natAbs b ↔ -a = bsimpa only [
Int.natAbs_neg: ∀ (a : ℤ), natAbs (-a) = natAbs a
Int.natAbs_neg] using 
natAbs_inj_of_nonneg_of_nonneg: ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → (natAbs a = natAbs b ↔ a = b)
natAbs_inj_of_nonneg_of_nonneg (
neg_nonneg_of_nonpos: ∀ {α : Type ?u.4523} [inst : OrderedAddCommGroup α] {a : α}, a ≤ 0 → 0 ≤ -a
neg_nonneg_of_nonpos 
ha: a ≤ 0
ha) 
hb: 0 ≤ b
hb
Goals accomplished! 🐙
#align int.nat_abs_inj_of_nonpos_of_nonneg 
Int.natAbs_inj_of_nonpos_of_nonneg: ∀ {a b : ℤ}, a ≤ 0 → 0 ≤ b → (natAbs a = natAbs b ↔ -a = b)
Int.natAbs_inj_of_nonpos_of_nonneg

section Intervals

open Set

theorem 
strictMonoOn_natAbs: StrictMonoOn natAbs (Ici 0)
strictMonoOn_natAbs : 
StrictMonoOn: {α : Type ?u.4705} → {β : Type ?u.4704} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → Prop
StrictMonoOn 
natAbs: ℤ → ℕ
natAbs (
Ici: {α : Type ?u.4753} → [inst : Preorder α] → α → Set α
Ici 
0: ?m.4779
0) := fun 
_: ?m.4869
_ 
ha: ?m.4872
ha 
_: ?m.4875
_ 
_: ?m.4878
_ 
hab: ?m.4881
hab =>
  
natAbs_lt_natAbs_of_nonneg_of_lt: ∀ {a b : ℤ}, 0 ≤ a → a < b → natAbs a < natAbs b
natAbs_lt_natAbs_of_nonneg_of_lt 
ha: ?m.4872
ha 
hab: ?m.4881
hab
#align int.strict_mono_on_nat_abs 
Int.strictMonoOn_natAbs: StrictMonoOn natAbs (Ici 0)
Int.strictMonoOn_natAbs

theorem 
strictAntiOn_natAbs: StrictAntiOn natAbs (Iic 0)
strictAntiOn_natAbs : 
StrictAntiOn: {α : Type ?u.4915} → {β : Type ?u.4914} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → Prop
StrictAntiOn 
natAbs: ℤ → ℕ
natAbs (
Iic: {α : Type ?u.4963} → [inst : Preorder α] → α → Set α
Iic 
0: ?m.4989
0) := fun 
a: ?m.5079
a 
_: ?m.5082
_ 
b: ?m.5085
b 
hb: ?m.5088
hb 
hab: ?m.5091
hab => by
Goals accomplished! 🐙
  
a✝, b✝: ℤ

n: ℕ

a: ℤ

x✝: a ∈ Iic 0

b: ℤ

hb: b ∈ Iic 0

hab: a < b

natAbs b < natAbs asimpa [
Int.natAbs_neg: ∀ (a : ℤ), natAbs (-a) = natAbs a
Int.natAbs_neg] using
    
natAbs_lt_natAbs_of_nonneg_of_lt: ∀ {a b : ℤ}, 0 ≤ a → a < b → natAbs a < natAbs b
natAbs_lt_natAbs_of_nonneg_of_lt (
Right.nonneg_neg_iff: ∀ {α : Type ?u.5202} [inst : AddGroup α] [inst_1 : LE α]
  [inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, 0 ≤ -a ↔ a ≤ 0
Right.nonneg_neg_iff.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr 
hb: b ∈ Iic 0
hb) (
neg_lt_neg_iff: ∀ {α : Type ?u.5288} [inst : AddGroup α] [inst_1 : LT α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
  [inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α}, -a < -b ↔ b < a
neg_lt_neg_iff.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr 
hab: a < b
hab)
Goals accomplished! 🐙
#align int.strict_anti_on_nat_abs 
Int.strictAntiOn_natAbs: StrictAntiOn natAbs (Iic 0)
Int.strictAntiOn_natAbs

theorem 
injOn_natAbs_Ici: InjOn natAbs (Ici 0)
injOn_natAbs_Ici : 
InjOn: {α : Type ?u.6773} → {β : Type ?u.6772} → (α → β) → Set α → Prop
InjOn 
natAbs: ℤ → ℕ
natAbs (
Ici: {α : Type ?u.6779} → [inst : Preorder α] → α → Set α
Ici 
0: ?m.6805
0) :=
  
strictMonoOn_natAbs: StrictMonoOn natAbs (Ici 0)
strictMonoOn_natAbs.
injOn: ∀ {α : Type ?u.6854} {β : Type ?u.6855} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMonoOn f s → InjOn f s
injOn
#align int.inj_on_nat_abs_Ici 
Int.injOn_natAbs_Ici: InjOn natAbs (Ici 0)
Int.injOn_natAbs_Ici

theorem 
injOn_natAbs_Iic: InjOn natAbs (Iic 0)
injOn_natAbs_Iic : 
InjOn: {α : Type ?u.6957} → {β : Type ?u.6956} → (α → β) → Set α → Prop
InjOn 
natAbs: ℤ → ℕ
natAbs (
Iic: {α : Type ?u.6963} → [inst : Preorder α] → α → Set α
Iic 
0: ?m.6989
0) :=
  
strictAntiOn_natAbs: StrictAntiOn natAbs (Iic 0)
strictAntiOn_natAbs.
injOn: ∀ {α : Type ?u.7038} {β : Type ?u.7039} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictAntiOn f s → InjOn f s
injOn
#align int.inj_on_nat_abs_Iic 
Int.injOn_natAbs_Iic: InjOn natAbs (Iic 0)
Int.injOn_natAbs_Iic

end Intervals

/-! ### `toNat` -/


theorem 
toNat_of_nonpos: ∀ {z : ℤ}, z ≤ 0 → toNat z = 0
toNat_of_nonpos : ∀ {
z: ℤ
z : 
ℤ: Type
ℤ}, 
z: ℤ
z ≤ 
0: ?m.7146
0 → 
z: ℤ
z.
toNat: ℤ → ℕ
toNat = 
0: ?m.7178
0
  | 
0: ℤ
0, _ => 
rfl: ∀ {α : Sort ?u.7219} {a : α}, a = a
rfl
  | (
n: ℕ
n + 1 : ℕ), 
h: ↑(n + 1) ≤ 0
h => (
h: ↑(n + 1) ≤ 0
h.
not_lt: ∀ {α : Type ?u.7366} [inst : Preorder α] {a b : α}, a ≤ b → ¬b < a
not_lt (by
Goals accomplished! 🐙 
a, b: ℤ

n✝, n: ℕ

h: ↑(n + 1) ≤ 0

0 < ↑(n + 1)simp
Goals accomplished! 🐙)).
elim: ∀ {C : Sort ?u.7423}, False → C
elim
  | -[
n: ℕ
n+1], _ => 
rfl: ∀ {α : Sort ?u.7445} {a : α}, a = a
rfl
#align int.to_nat_of_nonpos 
Int.toNat_of_nonpos: ∀ {z : ℤ}, z ≤ 0 → toNat z = 0
Int.toNat_of_nonpos

/-! ### bitwise ops

This lemma is orphaned from `Data.Int.Bitwise` as it also requires material from `Data.Int.Order`.
-/


attribute [local simp] 
Int.zero_div: ∀ (b : ℤ), div 0 b = 0
Int.zero_div

@[simp]
theorem 
div2_bit: ∀ (b : Bool) (n : ℤ), div2 (bit b n) = n
div2_bit (
b: Bool
b 
n: ?m.8026
n) : 
div2: ℤ → ℤ
div2 (
bit: Bool → ℤ → ℤ
bit 
b: ?m.8023
b 
n: ?m.8026
n) = 
n: ?m.8026
n := by
Goals accomplished! 🐙
  
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

div2 (bit b n) = nrw [
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

div2 (bit b n) = n
bit_val: ∀ (b : Bool) (n : ℤ), bit b n = 2 * n + bif b then 1 else 0
bit_val,
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

div2 (2 * n + bif b then 1 else 0) = n 
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

div2 (bit b n) = n
div2_val: ∀ (n : ℤ), div2 n = n / 2
div2_val,
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

(2 * n + bif b then 1 else 0) / 2 = n 
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

div2 (bit b n) = n
add_comm: ∀ {G : Type ?u.8051} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm,
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

((bif b then 1 else 0) + 2 * n) / 2 = n 
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

div2 (bit b n) = n
Int.add_mul_ediv_left: ∀ (a : ℤ) {b : ℤ} (c : ℤ), b ≠ 0 → (a + b * c) / b = a / b + c
Int.add_mul_ediv_left,
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

(bif b then 1 else 0) / 2 + n = n
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

H
2 ≠ 0 
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

div2 (bit b n) = n(
_: ?m.8121 / 2 = 0
_ : (
_: ?m.8120
_ / 
2: ?m.8123
2 : 
ℤ: Type
ℤ) = 
0: ?m.8183
0),
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

0 + n = n
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

(bif b then 1 else 0) / 2 = 0
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

H
2 ≠ 0 
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

div2 (bit b n) = n
zero_add: ∀ {M : Type ?u.8207} [inst : AddZeroClass M] (a : M), 0 + a = a
zero_add
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

n = n
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

(bif b then 1 else 0) / 2 = 0
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

H
2 ≠ 0]
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

(bif b then 1 else 0) / 2 = 0
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

H
2 ≠ 0
  
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

div2 (bit b n) = ncases 
b: Bool
b
a, b: ℤ

n✝: ℕ

n: ℤ

false
(bif false then 1 else 0) / 2 = 0
a, b: ℤ

n✝: ℕ

n: ℤ

true
(bif true then 1 else 0) / 2 = 0
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

H
2 ≠ 0
  
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

div2 (bit b n) = n·
a, b: ℤ

n✝: ℕ

n: ℤ

false
(bif false then 1 else 0) / 2 = 0 
a, b: ℤ

n✝: ℕ

n: ℤ

false
(bif false then 1 else 0) / 2 = 0
a, b: ℤ

n✝: ℕ

n: ℤ

true
(bif true then 1 else 0) / 2 = 0
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

H
2 ≠ 0simp
Goals accomplished! 🐙
  
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

div2 (bit b n) = n·
a, b: ℤ

n✝: ℕ

n: ℤ

true
(bif true then 1 else 0) / 2 = 0 
a, b: ℤ

n✝: ℕ

n: ℤ

true
(bif true then 1 else 0) / 2 = 0
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

H
2 ≠ 0show 
ofNat: ℕ → ℤ
ofNat 
_: ℕ
_ = 
_: ?m.8368
_
a, b: ℤ

n✝: ℕ

n: ℤ

true
ofNat (1 / 2) = 0
    
a, b: ℤ

n✝: ℕ

n: ℤ

true
(bif true then 1 else 0) / 2 = 0rw [
a, b: ℤ

n✝: ℕ

n: ℤ

true
ofNat (1 / 2) = 0
Nat.div_eq_zero: ∀ {a b : ℕ}, a < b → a / b = 0
Nat.div_eq_zero
a, b: ℤ

n✝: ℕ

n: ℤ

true
ofNat 0 = 0
a, b: ℤ

n✝: ℕ

n: ℤ

true
1 < 2]
a, b: ℤ

n✝: ℕ

n: ℤ

true
ofNat 0 = 0
a, b: ℤ

n✝: ℕ

n: ℤ

true
1 < 2 
a, b: ℤ

n✝: ℕ

n: ℤ

true
ofNat (1 / 2) = 0<;>
a, b: ℤ

n✝: ℕ

n: ℤ

true
ofNat 0 = 0
a, b: ℤ

n✝: ℕ

n: ℤ

true
1 < 2 
a, b: ℤ

n✝: ℕ

n: ℤ

true
ofNat (1 / 2) = 0simp
Goals accomplished! 🐙
  
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

div2 (bit b n) = n·
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

H
2 ≠ 0 
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ

H
2 ≠ 0decide
Goals accomplished! 🐙
#align int.div2_bit 
Int.div2_bit: ∀ (b : Bool) (n : ℤ), div2 (bit b n) = n
Int.div2_bit

end Int