Matrix operations, formalized in ACL2