| changeset 68072 | 493b818e8e10 |
| parent 67399 | eab6ce8368fa |
| child 68188 | 2af1f142f855 |
| 68001:0a2a1b6507c1 | 68072:493b818e8e10 |
|---|---|
6 section \<open>Bertrand's Ballot Theorem\<close> |
6 section \<open>Bertrand's Ballot Theorem\<close> |
7 |
7 |
8 theory Ballot |
8 theory Ballot |
9 imports |
9 imports |
10 Complex_Main |
10 Complex_Main |
11 "HOL-Library.FuncSet" |
|
12 begin |
11 begin |
13 |
12 |
14 subsection \<open>Preliminaries\<close> |
13 subsection \<open>Preliminaries\<close> |
15 |
14 |
16 lemma card_bij': |
15 lemma card_bij': |