Adding new reasoning combinators

[JacquesCarette]

Fascinating how these next proofs are essentially the cancel and elim (left and right) combinators in Categories.Morphism.Reasoning !

Originally posted by @JacquesCarette in https://github.com/agda/agda-stdlib/pull/2251#discussion_r1469634123

The point would be that for binary operations for which we have congruence (i.e. everything above Magma), there are additional combinators that we can create. Even more above Semigroup, where we also get associativity, and also Monoid (unital).

So we should get more and more reasoning power as we move up.

EDIT: Categories.Morphism.Reasoning

[jamesmckinna]

Naming:

• Is cancel actually an instance of a Cancellative property?
• Is there a more memorable/less generic name than elim for the other one?

[JacquesCarette]

• No, as Cancellative have a different shape and cancel-left: x * y = e -> x * (y * z) = z for e a unit. It is a chain of assoc, apply on left, left-unit. (There's cancel-right too).
• elim-id would be slightly better. The comments above the definition of those combinators is

-- Introduce/Elimilate an equivalent-to-identity
-- on left, right or 'in the middle' of something existing