zmod 4 is 0123

Stream: new members

[Tianchen Zhao]

Hi all! I know it sounds like a silly question :joy: , but is there a quick and elegant way to prove any integers is 0, 1, 2 or 3 mod 4? Every time my proof will go into the original definition of modeq and % and it takes a lot of work. mod4.PNG

[Kevin Buzzard]

Probably you can use that it's less than 4 and >= 0 and then use something like interval_cases. You know that it's better to post fully working code in ``` triple backticks (with all imports -- #mwe) than to post screenshots -- with code people can just cut and paste.