# Zulip Chat Archive

## Stream: new members

### Topic: more casting issues

#### Alex Kontorovich (Apr 21 2020 at 23:35):

Can someone please help with this proof? I realize I'm using subtraction within naturals, but nothing I've tried has worked on this...

lemma z (n m :ℕ ): 1 + (↑m - ↑n)= (1 + ↑m) - ↑n := begin sorry, end

Thanks!

#### Dan Stanescu (Apr 22 2020 at 00:25):

@Alex Kontorovich I could make this work with some effort. You can probably trim this down to half the size by working on the goal instead of `G`

, and I can bet someone with more experience can prove it in a couple lines or so.

lemma z (n m :ℕ ): 1 + ((m:ℤ) - (n:ℤ)) = (1 + (m:ℤ)) - (n:ℤ) := begin have G : 1 + ((m:ℤ) - (n:ℤ)) = 1 + ((m:ℤ) - (n:ℤ)), refl, rw add_comm at G {occs := occurrences.pos [1]}, rw add_comm, have F : -↑n = (-1:ℤ)*↑n, norm_num, have E : ↑m - ↑n = ↑m + (-1:ℤ)*↑n, norm_num, linarith, rw E at G {occs := occurrences.pos [2]}, set zn := (-1:ℤ)*↑n with hzn, have D : 1 + (↑m + zn) = 1 + ↑m + zn, linarith, rw D at G, rw ← F at G, exact G, end

Without the casts it wouldn't be valid, of course:

#eval 1 + (0-1) -- 1 #eval (1+0) - 1 -- 0

#### Alex Kontorovich (Apr 22 2020 at 00:33):

Amazing, thank you! (Glad I wasn't missing something trivial...)

#### Dan Stanescu (Apr 22 2020 at 00:36):

These casting problems have a tendency to be tough because they're so counter-intuitive for most of us!

#### Bryan Gin-ge Chen (Apr 22 2020 at 00:43):

If you're willing to use mathlib:

import tactic lemma z (n m :ℕ ): 1 + ((m:ℤ) - (n:ℤ)) = (1 + (m:ℤ)) - (n:ℤ) := by ring

#### Alex J. Best (Apr 22 2020 at 00:56):

If you are casting to any add_group this is the lemma `add_sub`

in mathlib

lemma z (n m :ℕ ): 1 + ((↑m:ℤ) - ↑n)= (1 + ↑m) - ↑n := add_sub 1 (↑ m) (↑ n)

and `by library_search`

should find it for you.

Last updated: Dec 20 2023 at 11:08 UTC