last digit challenge

Stream: maths

[Kevin Buzzard]

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]

I think this is omega.

[Kevin Buzzard]

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]

I think we already have that lemma

[Kevin Buzzard]

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]

and a % n % n = a % n

[Chris Hughes]

nat.modeq.modeq_add I believe.

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

OK I can do it with mod_add_div :-)

[Kevin Buzzard]

Thanks Chris!

[Chris Hughes]

If you reorder it to forall a le 9, forall b le 9, it's dec_trivial

[Mario Carneiro]

aah, please no gratuitous case bash on 10