Mathlib: Nat.add_sub_cancel is not add_sub_cancel; div/mod lemma shapes

Checked with #check on Lean v4.35 + Mathlib. (1) Nat.add_sub_cancel : n + m - m = n, but root add_sub_cancel : a + (b - a) = b needs AddCommGroup, so on ℕ it fails with 'failed to synthesize AddCommGroup ℕ'. Nat.add_sub_cancel (also _left, Nat.sub_add_cancel, Nat.mul_div_cancel) is protected, so open Nat does not change which lemma the short name means. ℕ versions of the root shapes: add_tsub_cancel_left/right (no hypothesis), add_tsub_cancel_of_le or Nat.add_sub_cancel' (a ≤ b → a + (b - a) = b), tsub_add_cancel_of_le or Nat.sub_add_cancel (b - a + a = b). Root add_sub_cancel' is an unknown identifier. (2) Nat.div_add_mod m n : n * (m / n) + m % n = m, primed: m / n * n + m % n = m; Nat.mod_add_div m k : m % k + k * (m / k) = m, primed: m % k + m / k * k = m. Int.ediv_add_emod and Int.emod_add_ediv are unknown constants; the Int names are Int.mul_ediv_add_emod a b : b * (a / b) + a % b = a and Int.emod_add_mul_ediv. (3) With 0 < k: Nat.le_div_iff_mul_le : x ≤ y / k ↔ x * k ≤ y and Nat.div_lt_iff_lt_mul : x / k < y ↔ x < y * k, but Nat.lt_div_iff_mul_lt : x < y / k ↔ x * k < y - (k - 1). (4) Finset.sum_range_succ puts f n on the right, sum_range_succ_comm on the left, sum_range_succ' peels off f 0 and shifts to f (k + 1).