lib-2.0-rc1: inconsistency of Nat..*-cancelˡ-≡ with AlmostLeftCancellative

[mechvel]

In Algebra.Definitions.AlmostLeftCancellative the order of the arguments x, y, z differs from such order in
Nat.Properties.*-cancelˡ-≡.
I suggest to change respectively this order in Nat.Properties.*-cancelˡ-≡.
Probably the same needs to be done to *-cancelʳ-≡.

It would be nice to set *-cancelˡ-≡ : AlmostLeftCancellative 0 _*_.
But unfortunately, the definition of "nonzero" for ℕ is not a special case of ≉ 0# in Semiring.

[jamesmckinna]

This is a duplicate of your still-open issue #1562 for which the core maintenance team reluctantly decided there was insufficient resource to fix for v2.0; our decision was that it be pushed to v3.0, the intended next label:breaking release of the library. Suggest your continue to comment, if necessary, on #1562 . Closing this one in the meantime.