mathlib

7c892653 - chore(data/list/range): Add range_zero and rename range_concat to range_succ (#5821)

chore(data/list/range): Add range_zero and rename range_concat to range_succ (#5821) The name `range_concat` was derived from `range'_concat`, where there are multiple possible expansions for `range' s n.succ`. For `range` there is only one choice, and naming the lemma after the result rather than the statement makes it harder to find.