Non-strict order equational reasoning

[hexwell]

Following #1203, this adds facilities for equational reasoning involving mixed use of <, ≤, ≡;
extracting a non-strict inequality instead of a strict one.

To extract a non-strict inequality, the additional data of <-≤-weaken is required (on top of what strict order already requires).

The same notes as the previous PR apply, noting that now:

• Either begin< or begin≤ is needed at the start of the chain, since it has to extract an inequality from the given chain.

Changelog

• The interface is now as follows:

  • Former <-≤-Reasoning renamed to <-≤-StrictReasoning
  • Former begin_ renamed to begin<_
  • Added new <-≤-Reasoning
  • Added new begin≤_

  Import <-≤-StrictReasoning if you only need to obtain strict inequalities,
  import <-≤-Reasoning otherwise.
  Use begin< to obtain a strict inequality (in this case, at least one < is required in the chain).
  Use begin≤ to obtain a nonstrict inequality.

• The SubRelation record has been deleted since it was out of place and not useful here, the instance has also been removed.

• Examples have been moved from a comment to a module, so that the compiler can check them for correctness in case of changes to the library.

[felixwellen]

In discussion, I was convinced there are applications for this -> merging this update.