theorem dvdmul12 (a b c: nat): $ a || b -> a || c * b $;
b || c * b
a || b -> b || c * b -> a || c * b
a || b -> a || c * b