(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)))))

(defmacro finite-natp (x n)
  `(and (natp ,x) (< ,x ,n)))

(defun finite-nat-listp (x n)
  (if (endp x)
      (null x)
      (and (finite-natp (car x) n)
           (finite-nat-listp (cdr x) n))))

(defun duplicatedp (x)
  (cond ((endp x) nil)
        ((member (car x) (cdr x)) t)
        (t (duplicatedp (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)))))

(defun map-count/list (x n)
  (if (zp n)
      nil
      (cons (count/list (1- n) x)
            (map-count/list (remove-equal (1- n) x) (1- n)))))

(defthm finite-nat-listp-remove-equal
  (implies (and (not (zp n))
                (finite-nat-listp x n))
           (and (finite-nat-listp (remove-equal (1- n) x) (1- n))
                (finite-nat-listp (remove-equal (1- n) x) n))))

(defthm len-map-count/list
  (implies (natp n)
           (equal (len (map-count/list x n)) n)))

(defthm sum-map-count/list-nil
  (equal (sum (map-count/list nil n)) 0))

(defun sum-map-count/list-induction (x n)
  (declare (xargs :measure (nfix n)))
  (if (zp n)
      x
      (sum-map-count/list-induction (remove-equal (1- n) x) (1- n))))

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

(defthm sum-map-count/list
  (implies (and (natp n)
                (finite-nat-listp x n))
           (equal (sum (map-count/list x n))
                  (len x)))
  :hints (("Goal" :induct (sum-map-count/list-induction x n))))

(defun map-count/list* (x n)
  (if (zp n)
      nil
      (cons (count/list (1- n) x)
            (map-count/list* x (1- n)))))

(defun nat-induction (n)
  (if (zp n)
      1
      (nat-induction (- n 1))))

(defthm duplicatedp-count/list
  (implies (< 1 (count/list e x))
           (duplicatedp x)))

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

(defthm duplicatedp-remove-equal
  (implies (duplicatedp (remove-equal e x))
           (duplicatedp x)))

(defthm member-if-over-1-map-count/list-is-duplicated
  (implies (and (natp n)
                (finite-nat-listp x n)
                (member-if-over-1 (map-count/list x n)))
           (duplicatedp x))
  :hints (("Goal" :induct (sum-map-count/list-induction x n))))

(defthm pigeonhole-for-finite-nat-list
  (implies (and (natp n)
                (finite-nat-listp x n)
                (< n (len x)))
           (duplicatedp x)))