Returns a candidate to be eliminated in step (2) of the IRV algorithm

- Signature
(candidate-with-least-nth-place-votes n cids xs) → cid

- Arguments
`n`—nth preference under consideration.

Guard (natp n) .`cids`— Candidates relevant in this round of tie-breaking (in ascending order).

Guard (nat-listp cids) .`xs`—Guard (irv-ballot-p xs) .- Returns
`cid`—Type (acl2::maybe-natp cid) , given(and (natp n) (nat-listp cids) (irv-ballot-p xs)) .

This function encodes step (2) of the IRV algorithm. If it
can find exactly one candidate among

For example:

(candidate-with-least-nth-place-votes 0 '(1 2 3 4) '((1 2 3 4) (2 3 1 4) (3 2 1 4)))

Result: candidate 4

Reason: 4 has zero 0th-place votes.

(candidate-with-least-nth-place-votes 0 '(1 2 3) '((1 2 3) (1 3 2) (3 2 1) (3 2 1) (2 3 1)))

Result: candidate 2

Reason: 2 has the fewest number of 0th-place votes.

(candidate-with-least-nth-place-votes 0 '(1 2 3) '((1 2 3) (1 3 2) (3 2 1) (2 3 1)))

Result: candidate 2

Reason: 2 and 3 are tied for fewest number of 0th, 1st, and 2nd
place votes. So we pick 2, because it is lesser than 3.

Note that this function will not be called by irv on ballots where step (1) of the IRV algorithm applies, i.e., when there is a majority in the first-place votes.

**Function: **

(defun candidate-with-least-nth-place-votes (n cids xs) (declare (xargs :guard (and (natp n) (nat-listp cids) (irv-ballot-p xs)))) (let ((__function__ 'candidate-with-least-nth-place-votes)) (declare (ignorable __function__)) (b* (((when (endp cids)) nil) (n (lnfix n)) ((unless (< n (number-of-candidates xs))) (pick-candidate cids)) (count-alst (create-nth-choice-count-alist n cids xs)) (candidates-with-min-votes (candidates-with-min-votes count-alst))) (if (equal (len candidates-with-min-votes) 1) (car candidates-with-min-votes) (candidate-with-least-nth-place-votes (1+ n) candidates-with-min-votes xs)))))

**Theorem: **

(defthm maybe-natp-of-candidate-with-least-nth-place-votes (implies (and (natp n) (nat-listp cids) (irv-ballot-p xs)) (b* ((cid (candidate-with-least-nth-place-votes n cids xs))) (acl2::maybe-natp cid))) :rule-classes :rewrite)

**Theorem: **

(defthm candidates-with-min-votes-is-a-subset-of-cids (subsetp-equal (candidates-with-min-votes (create-nth-choice-count-alist n cids xs)) cids))

**Theorem: **

(defthm candidate-with-least-nth-place-votes-is-in-cids (b* ((cid (candidate-with-least-nth-place-votes n cids xs))) (implies cid (member-equal cid cids))))

**Theorem: **

(defthm candidate-with-least-nth-place-votes-returns-a-natp (implies (and (nat-listp cids) (consp cids) (irv-ballot-p xs)) (natp (candidate-with-least-nth-place-votes n cids xs))) :rule-classes (:rewrite :type-prescription))

- Candidates-with-min-votes
- Returns a list of candidates, if any, which received the minimum number of votes
- Pick-candidate-with-smallest-id
- Pick candidate with the smallest ID.