Stream: math-comp devs

Topic: Missing subnKK?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Pierre Roux (Apr 15 2023 at 20:44):

Isn't it an injectivity lemma? in which case what about subnI, like addnI?

view this post on Zulip Laurent Théry (Apr 15 2023 at 20:47):

look to me like eqn_add2l.

view this post on Zulip Pierre Roux (Apr 15 2023 at 20:50):

Right, the injectivity lemmas are implications, not equivalences.


Last updated: Jul 24 2024 at 12:02 UTC