(defun remove-nth (i xs)
   (if (or (zp i) (endp (rest xs)))
       (rest xs)
       (cons (first xs)
             (remove-nth (1- i) (rest xs)))))

(defthm remove-nth-shortens
   (implies (consp xs)
            (< (len (remove-nth i xs)) (len xs))))

:set-state-ok t

(defun shuffle-r (xs ys state)
   (declare (xargs :measure (len xs)))
   (if (endp xs)
       (mv ys state)
       (mv-let (idx state)
               (random$ (len xs) state)
          (shuffle-r (remove-nth idx xs)
                     (cons (nth idx xs) ys)
                     state))))

(defun shuffle (xs state)
   (shuffle-r xs nil state))

(defun cross-r (x ys)
   (if (endp ys)
       nil
       (cons (cons x (first ys))
             (cross-r x (rest ys)))))

(defun cross (xs ys)
   (if (or (endp xs) (endp ys))
       nil
       (append (cross-r (first xs) ys)
               (cross (rest xs) ys))))

(defun make-deck ()
   (cross '(ace 2 3 4 5 6 7 8 9 10 jack queen king)
          '(hearts diamonds clubs spades)))

(defun print-card (card)
   (cw "~x0 of ~x1~%" (car card) (cdr card)))

(defun print-deck (deck)
   (if (endp deck)
       nil
       (progn$ (print-card (first deck))
               (print-deck (rest deck)))))

(defun draw-from-deck (deck)
   (mv (first deck) (rest deck)))