Axiom muleq | index | src |

Multiplication respects equalty.

axiom muleq (a b c d: nat): $ a = b -> c = d -> a * c = b * d $;