Miscellaneous lemmas about the integers #
This file contains lemmas about integers, which require further imports than
Data.Int.Basic
or Data.Int.Order
.
succ
and pred
#
natAbs
#
theorem
Int.natAbs_inj_of_nonneg_of_nonneg
{a : ℤ}
{b : ℤ}
(ha : 0 ≤ a)
(hb : 0 ≤ b)
:
Int.natAbs a = Int.natAbs b ↔ a = b
theorem
Int.natAbs_inj_of_nonpos_of_nonpos
{a : ℤ}
{b : ℤ}
(ha : a ≤ 0)
(hb : b ≤ 0)
:
Int.natAbs a = Int.natAbs b ↔ a = b
theorem
Int.natAbs_inj_of_nonneg_of_nonpos
{a : ℤ}
{b : ℤ}
(ha : 0 ≤ a)
(hb : b ≤ 0)
:
Int.natAbs a = Int.natAbs b ↔ a = -b
theorem
Int.natAbs_inj_of_nonpos_of_nonneg
{a : ℤ}
{b : ℤ}
(ha : a ≤ 0)
(hb : 0 ≤ b)
:
Int.natAbs a = Int.natAbs b ↔ -a = b
toNat
#
bitwise ops #
This lemma is orphaned from Data.Int.Bitwise
as it also requires material from Data.Int.Order
.