`VersionIsGreaterOrEqual` (or `CmpPlutusVersion`) is not expressive enough

[TotallyNotChase]

Describe the bug
VersionIsGreaterOrEqual is currently defined in such a way that it doesn't exhibit general properties like transitivity, commutativity etc. This is problematic when writing general wrappers around the Atlas machinery.

To Reproduce

Here's an example, I am trying to combine multiple GYBuildPlutusScript inputs into a unified transaction. Let's say I have GYBuildPlutusScript PlutusV2 and GYBuildPlutusScript PlutusV3, and I'm trying to just put them into one transaction. The resulting transaction would represent both as GYBuildPlutusScript PlutusV2, right? Now let's say I want to have a generalized function for this:

foo :: v1 `VersionIsGreaterOrEqual` v2 => GYBuildPlutusScript v1 -> GYBuildPlutusScript v2 -> [GYBuildPlutusScript v2] 
foo (GYBuildPlutusScriptInlined x) b = [res , b]
  where
    res :: GYBuildPlutusScript v2
    res = GYBuildPlutusScriptInlined x

I omitted the other constructor for brevity.

GHC needs to infer that the existential the v in x :: GYScript v satisfies v > v2 in order to type check res.
GHC knows v > v1, and it knows v1 > v2. Of course, this must mean v > v2 - but that's simply not infer-able by GHC because the > operator in this context is not defined to be transitive.

Expected behavior
Just works.

Screenshots

Station (please complete the following information):
Not relevant

Additional context
It seems to be that the PlutusVersion comparison stuff needs an overhaul.