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
it is a consequence of
eqn_sub2lE would be a better name.
Isn't it an injectivity lemma? in which case what about
look to me like
Right, the injectivity lemmas are implications, not equivalences.
Last updated: Nov 29 2023 at 22:01 UTC