# Documentation

Mathlib.Init.Data.Int.CompLemmas

# Auxiliary lemmas for proving that two int numerals are different #

1. Lemmas for reducing the problem to the case where the numerals are positive
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
1. Lemmas for proving that positive int numerals are nonneg and positive
theorem Int.one_pos :
0 < 1
@[deprecated]
theorem Int.bit0_pos {a : } :
0 < a0 < bit0 a
@[deprecated]
theorem Int.bit1_pos {a : } :
0 a0 < bit1 a
@[deprecated]
theorem Int.bit0_nonneg {a : } :
0 a0 bit0 a
@[deprecated]
theorem Int.bit1_nonneg {a : } :
0 a0 bit1 a
theorem Int.nonneg_of_pos {a : } :
0 < a0 a
1. Int.natAbs auxiliary lemmas
theorem Int.zero_le_ofNat (n : ) :
0
theorem Int.ne_of_natAbs_ne_natAbs_of_nonneg {a : } {b : } (ha : 0 a) (hb : 0 b) (h : ) :
a b
theorem Int.ne_of_nat_ne_nonneg_case {a : } {b : } {n : } {m : } (ha : 0 a) (hb : 0 b) (e1 : = n) (e2 : = m) (h : n m) :
a b
1. Aux lemmas for pushing Int.natAbs inside numerals Int.natAbs_zero and Int.natAbs_one are defined in Std4 and aligned in Matlib/Init/Data/Int/Basic.lean
theorem Int.natAbs_add_nonneg {a : } {b : } :
0 a0 bInt.natAbs (a + b) =
theorem Int.natAbs_add_neg {a : } {b : } :
a < 0b < 0Int.natAbs (a + b) =
@[deprecated]
theorem Int.natAbs_bit0 (a : ) :
@[deprecated]
theorem Int.natAbs_bit0_step {a : } {n : } (h : = n) :
@[deprecated]
theorem Int.natAbs_bit1_nonneg {a : } (h : 0 a) :
@[deprecated]
theorem Int.natAbs_bit1_nonneg_step {a : } {n : } (h₁ : 0 a) (h₂ : = n) :