I had to make a specific proof for the following lemma:

```
Lemma subnKK n m p : m <= n -> p <= n -> (n - m == n - p) = (m == p).
```

Is it worth a PR or did I just miss an obvious rewriting in `nat.v`

?

it is a consequence of `eqn_leq`

and `leq_sub2lE`

maybe `eqn_sub2lE`

would be a better name.

Isn't it an injectivity lemma? in which case what about `subnI`

, like `addnI`

?

look to me like `eqn_add2l`

.

Right, the injectivity lemmas are implications, not equivalences.

Last updated: Nov 29 2023 at 22:01 UTC