Miscellaneous lemmas about the integers

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

theorem Int.le_coe_nat_sub (m : ℕ) (n : ℕ) : ↑m - ↑n ≤ ↑(m - n)

succ and pred

theorem Int.succ_coe_nat_pos (n : ℕ) : 0 < ↑n + 1

natAbs

theorem Int.natAbs_eq_iff_sq_eq {a : ℤ} {b : ℤ} : Int.natAbs a = Int.natAbs b ↔ a ^ 2 = b ^ 2

theorem Int.natAbs_lt_iff_sq_lt {a : ℤ} {b : ℤ} : Int.natAbs a < Int.natAbs b ↔ a ^ 2 < b ^ 2

theorem Int.natAbs_le_iff_sq_le {a : ℤ} {b : ℤ} : Int.natAbs a ≤ Int.natAbs b ↔ a ^ 2 ≤ b ^ 2

theorem Int.natAbs_inj_of_nonneg_of_nonneg {a : ℤ} {b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) : Int.natAbs a = Int.natAbs b ↔ a = b

theorem Int.natAbs_inj_of_nonpos_of_nonpos {a : ℤ} {b : ℤ} (ha : a ≤ 0) (hb : b ≤ 0) : Int.natAbs a = Int.natAbs b ↔ a = b

theorem Int.natAbs_inj_of_nonneg_of_nonpos {a : ℤ} {b : ℤ} (ha : 0 ≤ a) (hb : b ≤ 0) : Int.natAbs a = Int.natAbs b ↔ a = -b

theorem Int.natAbs_inj_of_nonpos_of_nonneg {a : ℤ} {b : ℤ} (ha : a ≤ 0) (hb : 0 ≤ b) : Int.natAbs a = Int.natAbs b ↔ -a = b

theorem Int.strictMonoOn_natAbs : StrictMonoOn Int.natAbs (Set.Ici 0)

theorem Int.strictAntiOn_natAbs : StrictAntiOn Int.natAbs (Set.Iic 0)

theorem Int.injOn_natAbs_Ici : Set.InjOn Int.natAbs (Set.Ici 0)

theorem Int.injOn_natAbs_Iic : Set.InjOn Int.natAbs (Set.Iic 0)

toNat

theorem Int.toNat_of_nonpos {z : ℤ} : z ≤ 0 → Int.toNat z = 0

bitwise ops

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

@[simp]

theorem Int.div2_bit (b : Bool) (n : ℤ) : Int.div2 (Int.bit b n) = n