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 : } :
a > 0b > 0-a b

theorem int.ne_neg_of_pos {a b : } :
a > 0b > 0a -b

theorem int.one_pos  :
1 > 0

theorem int.bit0_pos {a : } :
a > 0bit0 a > 0

theorem int.bit1_pos {a : } :
a 0bit1 a > 0

theorem int.zero_nonneg  :
0 0

theorem int.one_nonneg  :
1 0

theorem int.bit0_nonneg {a : } :
a 0bit0 a 0

theorem int.bit1_nonneg {a : } :
a 0bit1 a 0

theorem int.nonneg_of_pos {a : } :
a > 0a 0

theorem int.of_nat_ge_zero (n : ) :

theorem int.ne_of_nat_abs_ne_nat_abs_of_nonneg {a b : } (ha : a 0) (hb : b 0) (h : a.nat_abs b.nat_abs) :
a b

theorem int.ne_of_nat_ne_nonneg_case {a b : } {n m : } (ha : a 0) (hb : b 0) (e1 : a.nat_abs = n) (e2 : b.nat_abs = m) (h : n m) :
a b

theorem int.nat_abs_add_nonneg {a b : } :
a 0b 0(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 : a 0) :

theorem int.nat_abs_bit1_nonneg_step {a : } {n : } (h₁ : a 0) (h₂ : a.nat_abs = n) :