(defun member-if-over-1 (x)
  (cond ((endp x) nil)
        ((< 1 (car x)) x)
        (t (member-if-over-1 (cdr x)))))

(defun sum (x)
  (if (endp x)
      0
      (+ (car x)
         (sum (cdr x)))))

(defthm pigeonhole
  (implies (< (len x) (sum x))
           (member-if-over-1 x)))

(defun list-count (e x)
  (cond ((endp x) 0)
        ((equal e (car x)) (1+ (list-count e (cdr x))))
        (t (list-count e (cdr x)))))

(defthm member-remove
  (implies (not (equal x y))
           (iff (member x (remove y z))
                (member x z))))

(defthm no-duplicatesp-remove
  (implies (no-duplicatesp x)
           (no-duplicatesp (remove e x))))

(defun map-list-count (x s)
  (if (endp s)
      nil
      (cons (list-count (car s) x)
            (map-list-count (remove (car s) x) (cdr s)))))

(defthm len-map-list-count
  (equal (len (map-list-count x s))
         (len s)))

(defthm len-remove
  (equal (len (remove e x))
         (- (len x) (list-count e x))))

(defthm not-subsetp-remove
  (implies (not (subsetp (remove e x) y))
           (not (subsetp x (cons e y)))))

(defthm sum-map-list-count
  (implies (and (no-duplicatesp s)
                (subsetp x s))
           (equal (sum (map-list-count x s))
                  (len x)))
  :hints (("Goal" :induct (map-list-count x s))))

(defthm not-no-duplicatesp-list-count
  (implies (< 1 (list-count e x))
           (not (no-duplicatesp x))))

(defthm not-no-duplicatesp-remove
  (implies (not (no-duplicatesp (remove e x)))
           (not (no-duplicatesp x))))

(defthm member-if-over-1-map-list-count-is-duplicated
  (implies (and (no-duplicatesp s)
                (subsetp x s)
                (member-if-over-1 (map-list-count x s)))
           (not (no-duplicatesp x)))
  :hints (("Goal" :induct (map-list-count x s))))

(defthm pigeonhole-for-list
  (implies (and (no-duplicatesp s)
                (subsetp x s)
                (< (len s) (len x)))
           (not (no-duplicatesp x))))