Simple integer divisibility

Stream: Is there code for X?

[Meyer Zinn]

Hello, novice user here. Is there any quick theorem for a | b -> a | c -> forall w x, a | wb + xc? (i.e., divisibility of linear combinations)

[Kevin Buzzard]

That looks to me like an easy consequence of two theorems which are probably there: a | b -> a | w*b and a | b -> a | c -> a | (b+c)

[Johan Commelin]

I guess not directly, but with a combo of dvd_add and dvd_mul_(left|right) you should be able to get there.

[Kevin Buzzard]

(let us know if we've said enough)

[Adam Topaz]

You probably want docs#dvd_mul_of_dvd_left (as opposed to dvd_mul_left)

[Adam Topaz]

Or docs#dvd_mul_of_dvd_right

[Johan Commelin]

Oops, "I was always bad with names"

[Meyer Zinn]

Thanks for the help! Don't know why those eluded me for so long.