More work on Coq Proofs
Add multiplication by zero rules