Injectivity of subtraction in Nat?

Stream: new members

[Luiz Kazuo Takei]

Is there a lemma in Nat that states the result below?

h1 : b \le a
h2 : c \le a
h3 : a - b = a - c

then

b = c

[Aaron Liu]

@loogle (?a - _ : Nat) = ?a - _

[loogle]

:search: Nat.sub_eq_sub_min, Array.extract_eq_extract_left, and 2 more

[Aaron Liu]

I thought there would be something

[Aaron Liu]

Maybe you can compose two lemmas

[Aaron Liu]

@loogle "sub_eq", "iff"

[loogle]

:search: Nat.sub_eq_iff_eq_add, Nat.sub_eq_iff_eq_add', and 57 more

[Aaron Liu]

@loogle Nat, _ - _ + _, _+ _ - _, LE.le

[loogle]

:search: Nat.sub_add_comm, Vector.insertIdx_eraseIdx_of_ge, and 3 more

[Aaron Liu]

Yes you can use docs#Nat.sub_eq_iff_eq_add with docs#Nat.sub_add_comm to get rid of the subtraction

[Aaron Liu]

or I guess you could cast to int

[Damiano Testa]

Would docs#tsub_inj_left work?

[Aaron Liu]

we want the other side inj

[Aaron Liu]

the right inj

[Matt Diamond]

what about... docs#tsub_inj_right

[Matt Diamond]

I think that's it

[Damiano Testa]

Ah, yes, the variable that's not repeated is the one that gets reflected in the name!

[Luiz Kazuo Takei]

Yes! docs#tsub_inj_right is the good one.

Thanks a lot!

[Jireh Loreaux]

It's not a lemma, but just noting that grind solves this.

[Luiz Kazuo Takei]

I noticed that omega also works:

example (a b c : ℕ) (h1 : a ≤ c) (h2 : b ≤ c) (h3 : c - a = c - b) : a = b := by omega

[Jireh Loreaux]

probably grind should be preferred over omega. If you ever find an instance where the latter succeeds, but the former doesn't, I'm sure Kim Morrison will want to know.