mathlib documentation

core / init.data.int.comp_lemmas

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 < a0 < b-a b
theorem int.ne_neg_of_pos {a b : } :
0 < a0 < ba -b
theorem int.one_pos  :
0 < 1
theorem int.bit0_pos {a : } :
0 < a0 < bit0 a
theorem int.bit1_pos {a : } :
0 a0 < bit1 a
theorem int.zero_nonneg  :
0 0
theorem int.one_nonneg  :
0 1
theorem int.bit0_nonneg {a : } :
0 a0 bit0 a
theorem int.bit1_nonneg {a : } :
0 a0 bit1 a
theorem int.nonneg_of_pos {a : } :
0 < a0 a
theorem int.zero_le_of_nat (n : ) :
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
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
theorem int.nat_abs_add_nonneg {a b : } :
0 a0 b(a + b).nat_abs = a.nat_abs + b.nat_abs
theorem int.nat_abs_add_neg {a b : } :
a < 0b < 0(a + b).nat_abs = a.nat_abs + b.nat_abs
theorem int.nat_abs_bit0 (a : ) :
theorem int.nat_abs_bit0_step {a : } {n : } (h : a.nat_abs = n) :
theorem int.nat_abs_bit1_nonneg {a : } (h : 0 a) :
theorem int.nat_abs_bit1_nonneg_step {a : } {n : } (h₁ : 0 a) (h₂ : a.nat_abs = n) :