A Machine-Checked Proof of the Odd Order Theorem