mul0r Show Code edit
## Multiply by 0
thm (mul0r () () (= (* (0) A) (0))
A mul0
(= (* A (0)) (0))
## <d 'Commutative Property '>
A (0) mulcom
(= (* A (0)) (* (0) A))
EqReplaceEq0
(= (* (0) A) (0))
## </d 'Commutative Property '>
)
edit