feat(data/{nat,list}/basic): Add some trivial lemmas (#4738)

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/data/list/basic.lean

@@ -1981,6 +1981,28 @@ lemma prod_update_nth : ∀ (L : list α) (n : ℕ) (a : α),
 
 end monoid
 
+section group
+variables [group α]
+
+/-- This is the `list.prod` version of `mul_inv_rev` -/
+@[to_additive "This is the `list.sum` version of `add_neg_rev`"]
+lemma prod_inv_reverse : ∀ (L : list α), L.prod⁻¹ = (L.map (λ x, x⁻¹)).reverse.prod
+| [] := by simp
+| (x :: xs) := by simp [prod_inv_reverse xs]
+
+end group
+
+section comm_group
+variables [comm_group α]
+
+/-- This is the `list.prod` version of `mul_inv` -/
+@[to_additive "This is the `list.sum` version of `add_neg`"]
+lemma prod_inv : ∀ (L : list α), L.prod⁻¹ = (L.map (λ x, x⁻¹)).prod
+| [] := by simp
+| (x :: xs) := by simp [mul_comm, prod_inv xs]
+
+end comm_group
+
 @[simp]
 lemma sum_take_add_sum_drop [add_monoid α] :
   ∀ (L : list α) (i : ℕ), (L.take i).sum + (L.drop i).sum = L.sum

src/data/nat/basic.lean

@@ -384,6 +384,10 @@ theorem sub_add_min (n m : ℕ) : n - m + min n m = n :=
 protected theorem add_sub_cancel' {n m : ℕ} (h : m ≤ n) : m + (n - m) = n :=
 by rw [add_comm, nat.sub_add_cancel h]
 
+protected theorem sub_add_sub_cancel {a b c : ℕ} (hab : b ≤ a) (hbc : c ≤ b) :
+  (a - b) + (b - c) = a - c :=
+by rw [←nat.add_sub_assoc hbc, ←nat.sub_add_comm hab, nat.add_sub_cancel]
+
 protected theorem sub_eq_of_eq_add (h : k = m + n) : k - m = n :=
 begin rw [h, nat.add_sub_cancel_left] end