[ refactor ] Rename+deprecate Algebra.Definition.Star*Expansive and Algebra.Definition.Star*Destructive

[jamesmckinna]

This is a backwards compatible first step towards fixing #3003 : (so not actually fixing a bug as such, more infrastructure on the way to doing so)

• moves the various definitions from Algebra.Definitions to Relation.Binary.Definitions, with an additional _≤_ : Rel A ℓ₁ parameter
• deprecates the old versions in Algebra.Definitions
• refactors Algebra.Structures.KleeneAlgebra to plumb in the existing equality as the new relational parameter.

This is an interim step, intended as low-hanging-fruit to review and merge, before considering larger-scale non-backwards-compatible restructuring to support the Kozen inequational axiomatisation of IsKleeneAlgebra in terms of the _≤_ definable in any IsCommutativeBand.

[JacquesCarette]

When I first saw this come through, I thought "what!?!?" and paused before posting to think about it further. Then more happened (especially with #3031 ) that made it all come together. So now I'm on board with this change.

[jamesmckinna]

@Taneb what's your take on my refactoring of KleeneAlgebra?

This PR is really 'only' hygiene, and hopefully can be merged without too much hand-wringing... but I can see it might appear pointless were it not then used in anger in #3031 but that's quite a bit more work to digest.

Separately!