Some basic facts about integers

int_lemmas.lean

-- Addition

theorem add_comm : ∀ (n m : Int), n + m = m + n := by
  intro n m
  simp [HAdd.hAdd, Add.add]
  match n, m with
  | Int.ofNat m,   Int.ofNat n   =>
    simp [Int.add]
    apply Nat.add_comm
  | Int.ofNat m,   Int.negSucc n =>
    simp [Int.add]
  | Int.negSucc m, Int.ofNat n   =>
    simp [Int.add]
  | Int.negSucc m, Int.negSucc n =>
    simp [Int.add]
    apply Nat.add_comm

@[simp] theorem zero_add : ∀ (n : Int), 0 + n = n := by
  intro n
  cases n with
  | ofNat m =>
    simp [HAdd.hAdd, Add.add, Int.add]
    simp
  | negSucc m =>
    simp [HAdd.hAdd, Add.add, Int.add, Int.subNatNat]

@[simp] theorem add_zero (n : Int) : n + 0 = n := by
  rw [add_comm n 0, zero_add n]


-- Multiplication

@[simp] theorem mul_zero (n : Int) : n * 0 = 0 := by
  simp [HMul.hMul, Mul.mul, OfNat.ofNat, Int.mul]
  cases n <;> simp

theorem mul_comm : ∀ (n m : Int), n * m = m * n := by
  intro m n
  simp [HMul.hMul, Mul.mul]
  match m, n with
  | Int.ofNat m,   Int.ofNat n   =>
    simp [Int.mul]
    apply Nat.mul_comm
  | Int.ofNat m,   Int.negSucc n =>
    simp [Int.mul]
    rw [Nat.mul_comm]
  | Int.negSucc m, Int.ofNat n   =>
    simp [Int.mul]
    rw [Nat.mul_comm]
  | Int.negSucc m, Int.negSucc n =>
    simp [Int.mul]
    apply Nat.mul_comm

@[simp] theorem zero_mul : ∀ (n : Int), 0 * n = 0 := by
  intro n
  rw [mul_comm 0 n]
  apply mul_zero

@[simp] theorem mul_one : ∀ (n : Int), n * 1 = n := by
  intro n
  simp [HMul.hMul, Mul.mul, OfNat.ofNat, Int.mul]
  cases n <;> simp
  simp [Int.negOfNat]

@[simp] theorem one_mul (n : Int) : 1 * n = n :=
  mul_comm n 1 ▸ mul_one n