In this article we formalize the Bertrand’s Ballot Theorem based on [17]. Suppose that in an election we have two candidates:
This theorem is item #30 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.