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 : } :
0 a0 -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 : } :
a 0b 0a.nat_abs b.nat_absa b

theorem int.ne_of_nat_ne_nonneg_case {a b : } {n m : } :
a 0b 0a.nat_abs = nb.nat_abs = mn ma 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 : } :
a.nat_abs = n(bit0 a).nat_abs = bit0 n

theorem int.nat_abs_bit1_nonneg {a : } :
a 0(bit1 a).nat_abs = bit1 a.nat_abs

theorem int.nat_abs_bit1_nonneg_step {a : } {n : } :
a 0a.nat_abs = n(bit1 a).nat_abs = bit1 n