AlmostCancellative in Nat.Properties ?

[mechvel]

lib-1.7 has a general notion AlmostLeft(Right)Cancellative,
and it is used in *-cancelˡ-nonZero in IsCancellativeCommutativeSemiring.

On the other hand Nat.Properties has the definitions of kind.

*-cancelʳ-≡ :  ∀ m n {o} → m * suc o ≡ n * suc o → m ≡ n  

It has sense to add there *-cancelˡ-nonZero, *-cancelʳ-nonZero
having types AlmostLeft(Right)Cancellative,
and to add the instances of CancellativeCommutativeSemiring for Nat and Integer.
?

[Taneb]

I think this is a good idea. It should probably also be done for Integers and Rationals, if it hasn't already.

[mechvel]

The matter is also in that *-cancel...nonZero does rely on suc.
Many domains have not any sensible suc.

[jamesmckinna]

I think a useful reconciliation of this proposal with the instances arising for the concrete numerical types might be to systematically add
NonZero num <-> num ≢ 0# lemmas to their Properties, and work outwards from there? Eg towards also fixing #1436...? ... and #1175

... UPDATED or proceed as @JacquesCarette suggested on #1436 by generalising Almost... properties. Then there's a second problem: instances vs. implicit arguments.