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_natCast_sub (m n : ℕ) : ↑m - ↑n ≤ ↑(m - n)

succ and pred

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

natAbs

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

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

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

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

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

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

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

theorem Int.natAbs_coe_sub_coe_le_of_le {a b n : ℕ} (a_le_n : a ≤ n) (b_le_n : b ≤ n) : (↑a - ↑b).natAbs ≤ n

A specialization of abs_sub_le_of_nonneg_of_le for working with the signed subtraction of natural numbers.

theorem Int.natAbs_coe_sub_coe_lt_of_lt {a b n : ℕ} (a_lt_n : a < n) (b_lt_n : b < n) : (↑a - ↑b).natAbs < n

A specialization of abs_sub_lt_of_nonneg_of_lt for working with the signed subtraction of natural numbers.

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

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

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

theorem Int.injOn_natAbs_Iic : Set.InjOn natAbs (Set.Iic 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 : ℤ) : (bit b n).div2 = n

theorem Int.ediv_emod_unique' {a b r q : ℤ} (h : b ≠ 0) : a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < |b|

Like Int.ediv_emod_unique, but permitting negative b.