Pierre Jouvelot (Apr 15 2023 at 20:30): Pierre Jouvelot (Apr 15 2023 at 20:30):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?
Laurent Théry (Apr 15 2023 at 20:40):it is a consequence of eqn_leq and leq_sub2lE maybe eqn_sub2lE would be a better name.
Pierre Roux (Apr 15 2023 at 20:44):Isn't it an injectivity lemma? in which case what about subnI, like addnI?
Laurent Théry (Apr 15 2023 at 20:47):look to me like eqn_add2l.
Pierre Roux (Apr 15 2023 at 20:50):Right, the injectivity lemmas are implications, not equivalences.
Last updated: Nov 29 2023 at 22:01 UTC