mathlib3 documentation

core / init.data.int.comp_lemmas

Auxiliary lemmas for proving that two int numerals are differen #

  1. Lemmas for reducing the problem to the case where the numerals are positive
source
@[protected]
theorem int.ne_neg_of_ne {a b : ℤ} :
a ≠ b → -a ≠ -b
source
@[protected]
theorem int.neg_ne_zero_of_ne {a : ℤ} :
a ≠ 0 → -a ≠ 0
source
@[protected]
theorem int.zero_ne_neg_of_ne {a : ℤ} (h : 0 ≠ a) :
0 ≠ -a
source
@[protected]
theorem int.neg_ne_of_pos {a b : ℤ} :
0 < a → 0 < b → -a ≠ b
source
@[protected]
theorem int.ne_neg_of_pos {a b : ℤ} :
0 < a → 0 < b → a ≠ -b
  1. Lemmas for proving that positive int numerals are nonneg and positive
source
@[protected]
theorem int.one_pos  :
0 < 1
source
@[protected]
theorem int.bit0_pos {a : ℤ} :
0 < a → 0 < bit0 a
source
@[protected]
theorem int.bit1_pos {a : ℤ} :
0 ≤ a → 0 < bit1 a
source
@[protected]
theorem int.zero_nonneg  :
0 ≤ 0
source
@[protected]
theorem int.one_nonneg  :
0 ≤ 1
source
@[protected]
theorem int.bit0_nonneg {a : ℤ} :
0 ≤ a → 0 ≤ bit0 a
source
@[protected]
theorem int.bit1_nonneg {a : ℤ} :
0 ≤ a → 0 ≤ bit1 a
source
@[protected]
theorem int.nonneg_of_pos {a : ℤ} :
0 < a → 0 ≤ a
  1. nat_abs auxiliary lemmas
source
theorem int.neg_succ_of_nat_lt_zero (n : ℕ) :
-[1+ n] < 0
source
theorem int.zero_le_of_nat (n : ℕ) :
0 ≤ int.of_nat n
source
theorem int.of_nat_nat_abs_eq_of_nonneg {a : ℤ} :
0 ≤ a → int.of_nat a.nat_abs = a
source
theorem int.ne_of_nat_abs_ne_nat_abs_of_nonneg {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) (h : a.nat_abs ≠ b.nat_abs) :
a ≠ b
source
@[protected]
theorem int.ne_of_nat_ne_nonneg_case {a b : ℤ} {n m : ℕ} (ha : 0 ≤ a) (hb : 0 ≤ b) (e1 : a.nat_abs = n) (e2 : b.nat_abs = m) (h : n ≠ m) :
a ≠ b
  1. Aux lemmas for pushing nat_abs inside numerals nat_abs_zero and nat_abs_one are defined at init/data/int/basic.lean
source
theorem int.nat_abs_of_nat_core (n : ℕ) :
(int.of_nat n).nat_abs = n
source
theorem int.nat_abs_of_neg_succ_of_nat (n : ℕ) :
-[1+ n].nat_abs = n.succ
source
@[protected]
theorem int.nat_abs_add_nonneg {a b : ℤ} :
0 ≤ a → 0 ≤ b → (a + b).nat_abs = a.nat_abs + b.nat_abs
source
@[protected]
theorem int.nat_abs_add_neg {a b : ℤ} :
a < 0 → b < 0 → (a + b).nat_abs = a.nat_abs + b.nat_abs
source
@[protected]
theorem int.nat_abs_bit0 (a : ℤ) :
(bit0 a).nat_abs = bit0 a.nat_abs
source
@[protected]
theorem int.nat_abs_bit0_step {a : ℤ} {n : ℕ} (h : a.nat_abs = n) :
(bit0 a).nat_abs = bit0 n
source
@[protected]
theorem int.nat_abs_bit1_nonneg {a : ℤ} (h : 0 ≤ a) :
(bit1 a).nat_abs = bit1 a.nat_abs
source
@[protected]
theorem int.nat_abs_bit1_nonneg_step {a : ℤ} {n : ℕ} (h₁ : 0 ≤ a) (h₂ : a.nat_abs = n) :
(bit1 a).nat_abs = bit1 n