theorem muldiv3 (a b: nat): $ b || a -> b * (a // b) = a $;
b * (a // b) = a // b * b
b || a -> a // b * b = a
b || a -> b * (a // b) = a