## Stream: new members

### Topic: norm_num doesn't prove

#### Scott Morrison (May 15 2020 at 10:50):

example : 10 = (-1 : ℤ) % 11 :=
by norm_num


Should it?

Is it true?

#### Reid Barton (May 15 2020 at 10:51):

I guess it has to be true (but it wouldn't be true in C for example)

#### Jalex Stark (May 15 2020 at 11:39):

#reduce (-1 : ℤ) % 11 gives 10

#### Jalex Stark (May 15 2020 at 11:41):

example : 10 = (-1 : ℤ) % 11 :=
by refl

example : 10 = (21 : ℤ) % 11 :=
by norm_num


Last updated: May 06 2021 at 21:09 UTC