theorem truemul (a b: nat): $ true (a * b) <-> true a /\ true b $;
a * b != 0 <-> a != 0 /\ b != 0
true (a * b) <-> true a /\ true b