Strict order equational reasoning

[LorenzoMolena]

Facilities for equational reasoning involving mixed use of <, ≤, ≡ in a type that is both a quoset and a poset (with the additional data of <-≤-trans, ≤-<-trans ) to obtain a strict inequality (having at least a < in the chain).
This is inspired from Relation.Binary.Reasoning.PartialOrder of the Agda Standard Library.

Some notes:

• Compatibility with the existing equational reasoning already present in Prelude can be achieved with a nested chain of equations, as shown in the commented example.
  Such a chain can be written without nested equations, but it is not recomended, since it will perform a bunch of substs, and the combinators from Prelude (such as _ ≡[ i ]⟨ p i ⟩ _ ) cannot be used.
• begin is needed at the start of the chain, since it has to extract a strict inequality from the given chain.
• It should be easy to expand the code to also extract nonstrict inequalities, in that case a < won't be required in the chain.