NonemptyInterval.length_add

theorem NonemptyInterval.length_add : ∀ {α : Type u_2} [inst : OrderedAddCommGroup α] (s t : NonemptyInterval α), (s + t).length = s.length + t.length

This theorem states that for any ordered additive commutative group `α`, and for any two non-empty intervals `s` and `t` within this group, the length of the interval formed by adding `s` and `t` is equal to the sum of the lengths of `s` and `t`. In other words, the length function defined on non-empty intervals behaves distributively over interval addition.

More concisely: For any ordered additive commutative group `α` and non-empty intervals `s` and `t` within it, the length of `s + t` equals the sum of the lengths of `s` and `t`.