# mathlib3documentation

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
@[protected]
theorem int.ne_neg_of_ne {a b : } :
a b -a -b
@[protected]
theorem int.neg_ne_zero_of_ne {a : } :
a 0 -a 0
@[protected]
theorem int.zero_ne_neg_of_ne {a : } (h : 0 a) :
0 -a
@[protected]
theorem int.neg_ne_of_pos {a b : } :
0 < a 0 < b -a b
@[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
@[protected]
theorem int.one_pos  :
0 < 1
@[protected]
theorem int.bit0_pos {a : } :
0 < a 0 < bit0 a
@[protected]
theorem int.bit1_pos {a : } :
0 a 0 < bit1 a
@[protected]
theorem int.zero_nonneg  :
0 0
@[protected]
theorem int.one_nonneg  :
0 1
@[protected]
theorem int.bit0_nonneg {a : } :
0 a 0 bit0 a
@[protected]
theorem int.bit1_nonneg {a : } :
0 a 0 bit1 a
@[protected]
theorem int.nonneg_of_pos {a : } :
0 < a 0 a
1. nat_abs auxiliary lemmas
theorem int.zero_le_of_nat (n : ) :
0
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
@[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
@[protected]
theorem int.nat_abs_add_nonneg {a b : } :
0 a 0 b (a + b).nat_abs = a.nat_abs + b.nat_abs
@[protected]
theorem int.nat_abs_add_neg {a b : } :
a < 0 b < 0 (a + b).nat_abs = a.nat_abs + b.nat_abs
@[protected]
theorem int.nat_abs_bit0 (a : ) :
@[protected]
theorem int.nat_abs_bit0_step {a : } {n : } (h : a.nat_abs = n) :
@[protected]
theorem int.nat_abs_bit1_nonneg {a : } (h : 0 a) :
@[protected]
theorem int.nat_abs_bit1_nonneg_step {a : } {n : } (h₁ : 0 a) (h₂ : a.nat_abs = n) :