euclidean division

Stream: general

[Nicholas Scheel]

Is there a proof of Euclidean division (divmod) in the libraries somewhere? I've been looking around for theorems with mod in the core library and mathlib but couldn't find anything ...

[Simon Hudon]

Have you looked in init.data.nat.lemmas in the core library?

https://github.com/leanprover/lean/blob/master/library/init/data/nat/lemmas.lean#L660-L740

[Nicholas Scheel]

ahh that makes sense now, thanks! I must have glossed over it earlier

[Simon Hudon]

No problems! The naming scheme is fairly regular so if you search for _mod_ in the core library or mathlib, it should give you a good list of available lemmas. If you miss any, they're usually close to the ones you do find