(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 count/list (e x)
  (cond ((endp x) 0)
        ((equal e (car x)) (1+ (count/list e (cdr x))))
        (t (count/list 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-count/list (x s)
  (if (endp s)
      nil
      (cons (count/list (car s) x)
            (map-count/list (remove (car s) x) (cdr s)))))

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

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

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

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

(defthm not-no-duplicatesp-count/list
  (implies (< 1 (count/list 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-count/list-is-duplicated
  (implies (and (no-duplicatesp s)
                (subsetp x s)
                (member-if-over-1 (map-count/list x s)))
           (not (no-duplicatesp x)))
  :hints (("Goal" :induct (map-count/list x s))))

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