Make Relation.Binary.Structures.IsStrictTotalOrder consistent with the hierarchy

[MatthewDaggitt]

While trying to polish off #2098 I've run into the issue that the structure IsStrictTotalOrder doesn't inherit directly from IsStrictPartialOrder. Instead it has flattened fields that try to avoid having to have the user re-prove irreflexivity.

This has various irritating effects including multiple non-identical copies of certain proofs such as isStrictPartialOrder in StrictTotalOrder bundle.

We did have exactly the same problem with lattices in #1108, which we fixed by adding biased versions of the records that replicated the old structure. We should take advantage of v2.0 and implement the same solution for IsStrictTotalOrder

[jamesmckinna]

Interesting!
I'm even more glad you took charge of #2098 , as I wouldn't have had the (historical) insights to raise, never mind tackle, this issue ;-)