feat: bdiv and bmod lemmas (#6494)

This PR proves the basic theorems about the functions `Int.bdiv` and
`Int.bmod`.

For all integers `x` and all natural numbers `m`, we have:
- `Int.bdiv_add_bmod`: `m * bdiv x m + bmod x m = x` (which is stated in
the docstring for docs#Int.bdiv)
- `Int.bmod_add_bdiv`: `bmod x m + m * bdiv x m = x`
- `Int.bdiv_add_bmod'`: `bdiv x m * m + bmod x m = x`
- `Int.bmod_add_bdiv'`: `bmod x m + bdiv x m * m = x`
- `Int.bmod_eq_self_sub_mul_bdiv`: `bmod x m = x - m * bdiv x m`
- `Int.bmod_eq_self_sub_bdiv_mul`: `bmod x m = x - bdiv x m * m`

These theorems are all equivalent to each other by the basic properties
of addition, multiplication, and subtraction of integers.

The names `Int.bdiv_add_bmod`, `Int.bmod_add_bdiv`,
`Int.bdiv_add_bmod'`, and `Int.bmod_add_bdiv'` are meant to parallel the
names of the existing theorems docs#Int.tmod_add_tdiv,
docs#Int.tdiv_add_tmod, docs#Int.tmod_add_tdiv', and
docs#Int.tdiv_add_tmod'.

The names `Int.bmod_eq_self_sub_mul_bdiv` and
`Int.bmod_eq_self_sub_bdiv_mul` follow mathlib's naming conventions.
Note that there is already a theorem called docs#Int.bmod_def, so it
would not have been possible to parallel the name of the existing
theorem docs#Int.tmod_def.

See
https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/bdiv.20and.20bmod.

Closes #6493.

src/Init/Data/Int/DivModLemmas.lean

@@ -1098,6 +1098,32 @@ theorem bmod_def (x : Int) (m : Nat) : bmod x m =
     (x % m) - m :=
   rfl
 
+theorem bdiv_add_bmod (x : Int) (m : Nat) : m * bdiv x m + bmod x m = x := by
+  unfold bdiv bmod
+  split
+  · simp_all only [Nat.cast_ofNat_Int, Int.mul_zero, emod_zero, Int.zero_add, Int.sub_zero,
+      ite_self]
+  · dsimp only
+    split
+    · exact ediv_add_emod x m
+    · rw [Int.mul_add, Int.mul_one, Int.add_assoc, Int.add_comm m, Int.sub_add_cancel]
+      exact ediv_add_emod x m
+
+theorem bmod_add_bdiv (x : Int) (m : Nat) : bmod x m + m * bdiv x m = x := by
+  rw [Int.add_comm]; exact bdiv_add_bmod x m
+
+theorem bdiv_add_bmod' (x : Int) (m : Nat) : bdiv x m * m + bmod x m = x := by
+  rw [Int.mul_comm]; exact bdiv_add_bmod x m
+
+theorem bmod_add_bdiv' (x : Int) (m : Nat) : bmod x m + bdiv x m * m = x := by
+  rw [Int.add_comm]; exact bdiv_add_bmod' x m
+
+theorem bmod_eq_self_sub_mul_bdiv (x : Int) (m : Nat) : bmod x m = x - m * bdiv x m := by
+  rw [← Int.add_sub_cancel (bmod x m), bmod_add_bdiv]
+
+theorem bmod_eq_self_sub_bdiv_mul (x : Int) (m : Nat) : bmod x m = x - bdiv x m * m := by
+  rw [← Int.add_sub_cancel (bmod x m), bmod_add_bdiv']
+
 theorem bmod_pos (x : Int) (m : Nat) (p : x % m < (m + 1) / 2) : bmod x m = x % m := by
   simp [bmod_def, p]