Typing With Leftovers - a Mechanization of Intuitionistic Multiplicative-Additive Linear Logic