calculate with mod

Stream: general

[Jeremy Avigad]

What is the best way to prove (m * n) % n = 0 on nat? IIRC, the library used to have rules like these for calculating with mod, but now I can't find them. Am I missing something?

[Chris Hughes]

nat.mul_mod_left

[Chris Hughes]

In general, the files, data.nat.modeq and data.zmod.basic might help with this stuff.

[Jeremy Avigad]

Thanks!

[Scott Morrison]

by library_search agrees: mul_mod_left m n :-)

I've actually run into some robustness problems (works on lots of examples, mysteriously fails in some cases, in every fix I try breaks something else...) but hopefully coming soon.

[Patrick Massot]

You are great at writing teasers!

[Scott Morrison]

Sorry.. life keeps intervening. :-)

[Scott Morrison]

It occurred to me on the bike ride in that I should split library_search into a few PRs. I should be able to do one that covers 95% of cases that is nice and simple. Then I can later add the full on "let's do backwards reasoning with clever choices of the search pattern", if I ever get that to be robust. :-)