switching between % and |

Stream: Is there code for X?

[Ryan Gold]

Is there some lemma in the standard library I could call to show that iff (a % b = 0) then (a | b)? I've been having a lot of difficulty finding the right way to handle mod.

[Mario Carneiro]

I guess it would be called mod_eq_zero

[Mario Carneiro]

docs#nat.dvd_iff_mod_eq_zero, docs#int.dvd_iff_mod_eq_zero, docs#euclidean_domain.mod_eq_zero

[Adam Topaz]

Or the one to rule them all: docs#nat.div_add_mod

[Adam Topaz]

But you will need a few more characters of code to get to divisibility

[Yaël Dillies]

(deleted)