Permutations Improvement, Kronecker Commutation

[wjbs]

This pull request has two (non-independent) main parts:

Significantly improve handling of permutations. This includes splitting Permutations.v into several files. PermutationsBase.v is roughly equivalent to the original Permutations.v file without any reference to permutation matrices. PermutationInstances.v contains definitions of and results about a large number of permutations, as well as building off of PermutationAutomation.v to provide robust automatic simplification of permutations, including a robust Setoid instance for perm_eq, bounded extensional equality of functions. PermutationMatrices.v defines and proves results about the matrices associated to permutations. Associated to these updates are numerous proof repairs and improvements.

Implement kron_comm, which commutes the kronecker product. In particular, this is the (symmetric) braiding of the monoidal category of matrices under kronecker product. Numerous results are proven, many of which are consequences of the main naturality result, kron_comm n p × (A ⊗ B) = B ⊗ A × kron_comm o m (for appropriate dimensions and WF matrices).
This depends on a number of lemmas added to base files (such as Complex.v and particularly Modulus.v), and also leads to a number of improved proofs. Many (especially computational) proofs about swap are special cases of results about kron_comm and are sped up by applying the general results.

In addition to lemmas directly used by the above sections, many other small lemmas are added to various files. Some of these come from needs in VyZX, especially the development of bipermutations. Likewise, numerous proofs have been shortened or sped up across a number of files. This was not done in any particularly systematic way, but in each case the change was done carefully. Some small to moderate compilation time improvements (no doubt offset by added code from permutations and kron_comm) may be present.

[adrianleh]

Looks like the CI is failing for 8.16/8.17. It looks like it's not too bad to fix (at least the current error)