Added proof scripts. Found some more bugs..
Updated addition example