Add mulext1 to iset.mm
Add mulext1 to iset.mm

This follows straightforwardly from remulext1 and other theorems
we already have.

Includes mulreim as a lemma. The order of arguments here (for example,
B x. C versus C x. B ) was intended to be based on muladd , but
I'm not sure I picked the most consistent or most logical order.
On the other hand, I'm not completely sure what the best order
is, so I'll leave this one untouched for now.

metamath/set.mm,metamath/set.mm,metamath/set.mm