feat: prove that regular languages are closed under concatenation

[ctchou]

In this patch we prove that regular languages are closed under concatenation, by leveraging the results already proved about the infinite executions of the automata concatenation construction in NA/Concat.lean. In order to do so, we introduce the notion of a "total LTS", which means that the LTS has a next state for any given starting state and label, and a "LTS.totalize" construction that converts any LTS into a total LTS by adding a sink state and transitions from all states to the sink state. Then the notion of "total" and the "totalize" construction are generalized to NA. By "totalizing" NA's, we can extend any finite execution of a NA into an infinite execution and thus re-use the results already proved for infinite executions.

We expect the same technique to be applicable to NA/Loop.lean and allow us to prove that regular languages are closed under the Kleene-star. But that is for future work.