# Documentation

Mathlib.Data.Int.Lemmas

# Miscellaneous lemmas about the integers #

This file contains lemmas about integers, which require further imports than Data.Int.Basic or Data.Int.Order.

theorem Int.le_coe_nat_sub (m : ) (n : ) :
m - n ↑(m - n)

### succ and pred#

theorem Int.succ_coe_nat_pos (n : ) :
0 < n + 1

### natAbs#

theorem Int.natAbs_eq_iff_sq_eq {a : } {b : } :
a ^ 2 = b ^ 2
theorem Int.natAbs_lt_iff_sq_lt {a : } {b : } :
a ^ 2 < b ^ 2
theorem Int.natAbs_le_iff_sq_le {a : } {b : } :
a ^ 2 b ^ 2
theorem Int.natAbs_inj_of_nonneg_of_nonneg {a : } {b : } (ha : 0 a) (hb : 0 b) :
a = b
theorem Int.natAbs_inj_of_nonpos_of_nonpos {a : } {b : } (ha : a 0) (hb : b 0) :
a = b
theorem Int.natAbs_inj_of_nonneg_of_nonpos {a : } {b : } (ha : 0 a) (hb : b 0) :
a = -b
theorem Int.natAbs_inj_of_nonpos_of_nonneg {a : } {b : } (ha : a 0) (hb : 0 b) :
-a = b

### toNat#

theorem Int.toNat_of_nonpos {z : } :
z 0 = 0

### bitwise ops #

This lemma is orphaned from Data.Int.Bitwise as it also requires material from Data.Int.Order.

@[simp]
theorem Int.div2_bit (b : Bool) (n : ) :