A rigorous proof. Totally unimportant to the code, but I didn't want