Stuff for algebra.big_operators.ring

theorem sum_tsub {α : Type u_1} {β : Type u_2} [AddCommMonoid β] [PartialOrder β] [ExistsAddOfLE β] [CovariantClass β β (fun (x1 x2 : β) => x1 + x2) fun (x1 x2 : β) => x1 ≤ x2] [ContravariantClass β β (fun (x1 x2 : β) => x1 + x2) fun (x1 x2 : β) => x1 ≤ x2] [Sub β] [OrderedSub β] (s : Finset α) {f g : α → β} (hfg : ∀ x ∈ s, g x ≤ f x) : ∑ x ∈ s, (f x - g x) = ∑ x ∈ s, f x - ∑ x ∈ s, g x