Lemmas about integer division #
/
#
mod #
properties of /
and %
#
@[simp]
theorem
Int.natAbs_div
(a : Int)
(b : Int)
:
Int.natAbs (Int.div a b) = Nat.div (Int.natAbs a) (Int.natAbs b)
dvd #
@[simp]
Std.Data.Int.DivMod
/
#/
and %
#