Fix notations for MOVSX and MOVZX.

They are broken in the original CoqAsm formalization.