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.