# Zulip Chat Archive

## Stream: maths

### Topic: last digit challenge

#### Kevin Buzzard (Jan 29 2019 at 22:31):

Ali asked me about digits of nats (in base 10) today and I'm writing a little API for him, but this is a pain:

example (m n : ℕ) : (m + n) % 10 = 9 → m % 10 + n % 10 = 9 := sorry

These things are still far more painful than I'd like. In a 3rd year number theory class I'd even claim that this was "obvious". Should I be using ZMOD or something?

#### Chris Hughes (Jan 29 2019 at 22:33):

I think this is omega.

#### Kevin Buzzard (Jan 29 2019 at 22:34):

My plan was to prove `(m % 10 + n % 10) % 10 = 9`

and then do some case bash because `nat.mod_lt`

says n % 10 < 10. But I'm not sure how to do the case bash or prove this intermediate step.

#### Patrick Massot (Jan 29 2019 at 22:34):

I think we already have that lemma

#### Kevin Buzzard (Jan 29 2019 at 22:35):

I thought there were some lemmas like this but I can't find any that are useful to me. We have `(x + y * z) % y = x % y`

#### Kevin Buzzard (Jan 29 2019 at 22:36):

and `a % n % n = a % n`

#### Chris Hughes (Jan 29 2019 at 22:36):

nat.modeq.modeq_add I believe.

#### Kevin Buzzard (Jan 29 2019 at 22:36):

I'm trying to prove something for Ali so he can formalise his claimed proof that he's found the smallest positive integer which is a multiple of 91 and whose digit sum is also a multiple of 91.

#### Kevin Buzzard (Jan 29 2019 at 22:37):

ooh I've not even got that imported I suspect. So I'm not using the right tools by the looks of things.

#### Kevin Buzzard (Jan 29 2019 at 22:47):

Ok thanks Chris; I'm now down to `example (a b : ℕ) : a ≤ 9 → b ≤ 9 → (a + b) % 10 = 9 → a + b = 9 := sorry`

; I want to do this by `dec_trivial`

even though it's a bit lame; it would be better to show that a + b \le 18 and any solution to x % 10 = 9 other than 9 is >= 19.

#### Kevin Buzzard (Jan 29 2019 at 22:50):

now down to `e <= 18 -> e % 10 = 9 -> e = 9`

#### Kevin Buzzard (Jan 29 2019 at 22:51):

OK I can do it with mod_add_div :-)

#### Kevin Buzzard (Jan 29 2019 at 22:51):

Thanks Chris!

#### Chris Hughes (Jan 29 2019 at 22:59):

If you reorder it to `forall a le 9, forall b le 9`

, it's `dec_trivial`

#### Mario Carneiro (Jan 29 2019 at 23:52):

aah, please no gratuitous case bash on 10

Last updated: May 12 2021 at 08:14 UTC