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