Axiom
muleq
≪
|
index
|
src
|
≫
Multiplication respects equalty.
axiom muleq (a b c d: nat): $ a = b -> c = d -> a * c = b * d $;