Define the product of two LTSs

[ayberkt]

After #387, define the binary product in the category of LTSs.

[ctchou]

I just want to point out that there is already a product construction for nondeterministic automata in Automata/NA/Prod.lean, which may be related to the LTS product you want to define.