Auxiliary lemmas for proving that two int numerals are different

1. Lemmas for reducing the problem to the case where the numerals are positive

theorem Int.ne_neg_of_ne {a : ℤ} {b : ℤ} : a ≠ b → -a ≠ -b

theorem Int.neg_ne_zero_of_ne {a : ℤ} : a ≠ 0 → -a ≠ 0

theorem Int.zero_ne_neg_of_ne {a : ℤ} (h : 0 ≠ a) : 0 ≠ -a

theorem Int.neg_ne_of_pos {a : ℤ} {b : ℤ} : 0 < a → 0 < b → -a ≠ b

theorem Int.ne_neg_of_pos {a : ℤ} {b : ℤ} : 0 < a → 0 < b → a ≠ -b

2. Lemmas for proving that positive int numerals are nonneg and positive

theorem Int.one_pos : 0 < 1

@[deprecated]

theorem Int.bit0_pos {a : ℤ} : 0 < a → 0 < bit0 a

@[deprecated]

theorem Int.bit1_pos {a : ℤ} : 0 ≤ a → 0 < bit1 a

theorem Int.zero_nonneg : 0 ≤ 0

theorem Int.one_nonneg : 0 ≤ 1

@[deprecated]

theorem Int.bit0_nonneg {a : ℤ} : 0 ≤ a → 0 ≤ bit0 a

@[deprecated]

theorem Int.bit1_nonneg {a : ℤ} : 0 ≤ a → 0 ≤ bit1 a

theorem Int.nonneg_of_pos {a : ℤ} : 0 < a → 0 ≤ a

3. Int.natAbs auxiliary lemmas

theorem Int.zero_le_ofNat (n : ℕ) : 0 ≤ Int.ofNat n

theorem Int.ne_of_natAbs_ne_natAbs_of_nonneg {a : ℤ} {b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) (h : Int.natAbs a ≠ Int.natAbs b) : a ≠ b

theorem Int.ne_of_nat_ne_nonneg_case {a : ℤ} {b : ℤ} {n : ℕ} {m : ℕ} (ha : 0 ≤ a) (hb : 0 ≤ b) (e1 : Int.natAbs a = n) (e2 : Int.natAbs b = m) (h : n ≠ m) : a ≠ b

4. Aux lemmas for pushing Int.natAbs inside numerals Int.natAbs_zero and Int.natAbs_one are defined in Std4 and aligned in Matlib/Init/Data/Int/Basic.lean

theorem Int.natAbs_ofNat_core (n : ℕ) : Int.natAbs (Int.ofNat n) = n

theorem Int.natAbs_of_negSucc (n : ℕ) : Int.natAbs (Int.negSucc n) = Nat.succ n

theorem Int.natAbs_add_nonneg {a : ℤ} {b : ℤ} : 0 ≤ a → 0 ≤ b → Int.natAbs (a + b) = Int.natAbs a + Int.natAbs b

theorem Int.natAbs_add_neg {a : ℤ} {b : ℤ} : a < 0 → b < 0 → Int.natAbs (a + b) = Int.natAbs a + Int.natAbs b

@[deprecated]

theorem Int.natAbs_bit0 (a : ℤ) : Int.natAbs (bit0 a) = bit0 (Int.natAbs a)

@[deprecated]

theorem Int.natAbs_bit0_step {a : ℤ} {n : ℕ} (h : Int.natAbs a = n) : Int.natAbs (bit0 a) = bit0 n

@[deprecated]

theorem Int.natAbs_bit1_nonneg {a : ℤ} (h : 0 ≤ a) : Int.natAbs (bit1 a) = bit1 (Int.natAbs a)

@[deprecated]

theorem Int.natAbs_bit1_nonneg_step {a : ℤ} {n : ℕ} (h₁ : 0 ≤ a) (h₂ : Int.natAbs a = n) : Int.natAbs (bit1 a) = bit1 n