feat(algebra/group; data/nat) lemmas for sub sub assoc (#1712)

* Lemmas for sub sub assoc

* Removed a lemma

src/algebra/group/basic.lean

@@ -152,6 +152,9 @@ section add_group
   lemma sub_sub_sub_cancel_right (a b c : α) : (a - c) - (b - c) = a - b :=
   by rw [← neg_sub c b, sub_neg_eq_add, sub_add_sub_cancel]
 
+  theorem sub_sub_assoc_swap : a - (b - c) = a + c - b :=
+  by simp
+
   theorem sub_eq_zero : a - b = 0 ↔ a = b :=
   ⟨eq_of_sub_eq_zero, λ h, by rw [h, sub_self]⟩
 
@@ -205,9 +208,9 @@ section add_comm_group
 
   lemma add_sub_cancel'_right (a b : α) : a + (b - a) = b :=
   by rw [← add_sub_assoc, add_sub_cancel']
-  
+
   @[simp] lemma add_add_neg_cancel'_right (a b : α) : a + (b + -a) = b :=
-  add_sub_cancel'_right a b 
+  add_sub_cancel'_right a b
 
   lemma sub_right_comm (a b c : α) : a - b - c = a - c - b :=
   add_right_comm _ _ _

src/data/nat/basic.lean

@@ -185,6 +185,10 @@ by rw [add_comm a, nat.add_sub_assoc h, add_comm]
 theorem sub_min (n m : ℕ) : n - min n m = n - m :=
 nat.sub_eq_of_eq_add $ by rw [add_comm, sub_add_min]
 
+theorem sub_sub_assoc {a b c : ℕ} (h₁ : b ≤ a) (h₂ : c ≤ b) : a - (b - c) = a - b + c :=
+(nat.sub_eq_iff_eq_add (le_trans (nat.sub_le _ _) h₁)).2 $
+by rw [add_right_comm, add_assoc, nat.sub_add_cancel h₂, nat.sub_add_cancel h₁]
+
 protected theorem lt_of_sub_pos (h : 0 < n - m) : m < n :=
 lt_of_not_ge
   (assume : n ≤ m,
@@ -544,11 +548,11 @@ lemma succ_div : ∀ (a b : ℕ), (a + 1) / b =
     simp [hba, hb_le_a1, hb_dvd_a], }
 end
 
-lemma succ_div_of_dvd {a b : ℕ} (hba : b ∣ a + 1) : 
+lemma succ_div_of_dvd {a b : ℕ} (hba : b ∣ a + 1) :
   (a + 1) / b = a / b + 1 :=
 by rw [succ_div, if_pos hba]
 
-lemma succ_div_of_not_dvd {a b : ℕ} (hba : ¬ b ∣ a + 1) : 
+lemma succ_div_of_not_dvd {a b : ℕ} (hba : ¬ b ∣ a + 1) :
   (a + 1) / b = a / b :=
 by rw [succ_div, if_neg hba, add_zero]