(NOTE-LIB "wilson")

(DEFINE (^BM^SQUARES N P)
 (IF (^BM^ZEROP N)
     (^BM^CONS (^INT (^BM^ZERO)) (^NIL))
     (^BM^CONS (^BM^REMAINDER (^BM^TIMES N N) P) (^BM^SQUARES (^BM^SUB1 N) P))))

(DEFINE (^BM^RESIDUE A P)
 (^BM^AND (^BM^NOT (^BM^DIVIDES P A))
  (^BM^MEMBER (^BM^REMAINDER A P) (^BM^SQUARES P P))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP P)) (^BM^LEQ M N))
  (^BM^MEMBER (^BM^REMAINDER (^BM^TIMES M M) P) (^BM^SQUARES N P))))

(LEMMA
 (EQUAL (^BM^REMAINDER (^BM^TIMES Y Y) P)
        (^BM^REMAINDER (^BM^TIMES (^BM^REMAINDER Y P) (^BM^REMAINDER Y P)) P)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP P)) (^BM^NOT (^BM^MEMBER X (^BM^SQUARES P P))))
  (^BM^NOT (EQUAL X (^BM^REMAINDER (^BM^TIMES Y Y) P)))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P))
  (EQUAL (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO)))
          (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
         (^BM^SUB1 P))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P))
  (EQUAL (^BM^EXP (^BM^TIMES I I)
          (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
         (^BM^EXP I (^BM^SUB1 P)))))

(LEMMA
 (^BM^IMPLIES (EQUAL (^BM^REMAINDER A P) (^BM^REMAINDER B P))
  (EQUAL (^BM^REMAINDER (^BM^EXP A C) P) (^BM^REMAINDER (^BM^EXP B C) P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P))
    (^BM^NOT (^BM^DIVIDES P I))))
  (EQUAL (^BM^REMAINDER
          (^BM^EXP (^BM^TIMES I I)
           (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
          P)
         (^INT (^BM^CONS (^1) (^BM^ZERO))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P A))
    (EQUAL (^BM^REMAINDER A P) (^BM^REMAINDER (^BM^TIMES I I) P))))
  (^BM^NOT (^BM^DIVIDES P I))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P))
    (^BM^AND (^BM^NOT (^BM^DIVIDES P A))
     (EQUAL (^BM^REMAINDER A P) (^BM^REMAINDER (^BM^TIMES I I) P)))))
  (EQUAL (^BM^REMAINDER
          (^BM^EXP A (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))) P)
         (^INT (^BM^CONS (^1) (^BM^ZERO))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P))
    (^BM^AND (^BM^NOT (^BM^DIVIDES P A))
     (^BM^MEMBER (^BM^REMAINDER A P) (^BM^SQUARES I P)))))
  (EQUAL (^BM^REMAINDER
          (^BM^EXP A (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))) P)
         (^INT (^BM^CONS (^1) (^BM^ZERO))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P))
    (^BM^RESIDUE A P)))
  (EQUAL (^BM^REMAINDER
          (^BM^EXP A (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))) P)
         (^INT (^BM^CONS (^1) (^BM^ZERO))))))

(DEFINE (^BM^COMPLEMENT J A P)
 (^BM^REMAINDER (^BM^TIMES (^BM^INVERSE J P) A) P))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^PRIME P) (^BM^NOT (^BM^DIVIDES P J)))
  (EQUAL (^BM^REMAINDER (^BM^TIMES J (^BM^COMPLEMENT J A P)) P)
         (^BM^REMAINDER A P))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP P)) (^BM^LESSP (^BM^COMPLEMENT J A P) P)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P J)) (^BM^NOT (^BM^DIVIDES P A))))
  (^BM^NOT (^BM^ZEROP (^BM^COMPLEMENT J A P)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P A))
    (EQUAL (^BM^REMAINDER (^BM^TIMES J X) P) (^BM^REMAINDER A P))))
  (EQUAL (^BM^COMPLEMENT J A P) (^BM^REMAINDER X P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P J))
    (^BM^AND (^BM^NOT (^BM^DIVIDES P A)) (^BM^NOT (^BM^RESIDUE A P)))))
  (^BM^NOT (EQUAL J (^BM^COMPLEMENT J A P)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P J)) (^BM^NOT (^BM^DIVIDES P A))))
  (EQUAL (^BM^COMPLEMENT (^BM^COMPLEMENT J A P) A P) (^BM^REMAINDER J P))))

(DEFINE (^BM^COMP-LIST I A P)
 (IF (^BM^ZEROP I)
     (^NIL)
     (IF (^BM^MEMBER I (^BM^COMP-LIST (^BM^SUB1 I) A P))
         (^BM^COMP-LIST (^BM^SUB1 I) A P)
         (^BM^CONS I
          (^BM^CONS (^BM^COMPLEMENT I A P) (^BM^COMP-LIST (^BM^SUB1 I) A P))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P) (^BM^AND (^BM^LESSP I P) (^BM^NOT (^BM^DIVIDES P A))))
  (^BM^ALL-NON-ZEROP (^BM^COMP-LIST I A P))))

(LEMMA
 (^BM^IMPLIES (^BM^LESSP I P)
  (^BM^ALL-LESSEQP (^BM^COMP-LIST I A P) (^BM^SUB1 P))))

(LEMMA (^BM^SUBSETP (^BM^POSITIVES N) (^BM^COMP-LIST N A P)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^ZEROP I))
    (^BM^AND (^BM^LESSP I P)
     (^BM^AND (^BM^NOT (^BM^DIVIDES P A))
      (^BM^MEMBER J (^BM^COMP-LIST I A P))))))
  (^BM^MEMBER (^BM^COMPLEMENT J A P) (^BM^COMP-LIST I A P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^ZEROP I))
    (^BM^AND (^BM^NOT (^BM^ZEROP J))
     (^BM^AND (^BM^LESSP I P)
      (^BM^AND (^BM^LESSP J P)
       (^BM^AND (^BM^NOT (^BM^DIVIDES P A))
        (^BM^MEMBER (^BM^COMPLEMENT J A P) (^BM^COMP-LIST I A P))))))))
  (^BM^MEMBER J (^BM^COMP-LIST I A P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^LESSP I P)
    (^BM^AND (^BM^NOT (^BM^DIVIDES P A))
     (^BM^AND (^BM^NOT (^BM^RESIDUE A P))
      (^BM^ALL-DISTINCT (^BM^COMP-LIST (^BM^SUB1 I) A P))))))
  (^BM^ALL-DISTINCT (^BM^COMP-LIST I A P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^LESSP I P)
    (^BM^AND (^BM^NOT (^BM^DIVIDES P A)) (^BM^NOT (^BM^RESIDUE A P)))))
  (^BM^ALL-DISTINCT (^BM^COMP-LIST I A P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P A)) (^BM^NOT (^BM^RESIDUE A P))))
  (^BM^PERM (^BM^POSITIVES (^BM^SUB1 P)) (^BM^COMP-LIST (^BM^SUB1 P) A P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P A)) (^BM^NOT (^BM^RESIDUE A P))))
  (EQUAL (^BM^TIMES-LIST (^BM^COMP-LIST (^BM^SUB1 P) A P))
         (^BM^FACT (^BM^SUB1 P)))))

(LEMMA
 (^BM^IMPLIES (EQUAL (^BM^REMAINDER (^BM^TIMES I J) P) (^BM^REMAINDER A P))
  (EQUAL (^BM^REMAINDER (^BM^TIMES I (^BM^TIMES J K)) P)
         (^BM^REMAINDER (^BM^TIMES A (^BM^REMAINDER K P)) P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND
   (EQUAL (^BM^REMAINDER (^BM^TIMES I (^BM^COMPLEMENT I A P)) P)
          (^BM^REMAINDER A P))
   (^BM^AND (^BM^NOT (^BM^ZEROP I))
    (^BM^NOT (^BM^MEMBER I (^BM^COMP-LIST (^BM^SUB1 I) A P)))))
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^COMP-LIST I A P)) P)
         (^BM^REMAINDER
          (^BM^TIMES A
           (^BM^REMAINDER (^BM^TIMES-LIST (^BM^COMP-LIST (^BM^SUB1 I) A P)) P))
          P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P I))
    (^BM^NOT (^BM^MEMBER I (^BM^COMP-LIST (^BM^SUB1 I) A P)))))
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^COMP-LIST I A P)) P)
         (^BM^REMAINDER
          (^BM^TIMES A
           (^BM^REMAINDER (^BM^TIMES-LIST (^BM^COMP-LIST (^BM^SUB1 I) A P)) P))
          P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP N))
   (^BM^AND (^BM^NUMBERP X) (EQUAL Y (^BM^PLUS X N))))
  (EQUAL (^BM^QUOTIENT Y N) (^BM^ADD1 (^BM^QUOTIENT X N)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP I))
   (^BM^NOT (^BM^MEMBER I (^BM^COMP-LIST (^BM^SUB1 I) A P))))
  (EQUAL (^BM^QUOTIENT (^BM^LENGTH (^BM^COMP-LIST I A P))
          (^INT (^BM^CONS (^2) (^BM^ZERO))))
         (^BM^ADD1
          (^BM^QUOTIENT (^BM^LENGTH (^BM^COMP-LIST (^BM^SUB1 I) A P))
           (^INT (^BM^CONS (^2) (^BM^ZERO))))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^ZEROP I))
    (^BM^AND (^BM^LESSP I P)
     (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^COMP-LIST (^BM^SUB1 I) A P)) P)
            (^BM^REMAINDER
             (^BM^EXP A
              (^BM^QUOTIENT (^BM^LENGTH (^BM^COMP-LIST (^BM^SUB1 I) A P))
               (^INT (^BM^CONS (^2) (^BM^ZERO)))))
             P)))))
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^COMP-LIST I A P)) P)
         (^BM^REMAINDER
          (^BM^EXP A
           (^BM^QUOTIENT (^BM^LENGTH (^BM^COMP-LIST I A P))
            (^INT (^BM^CONS (^2) (^BM^ZERO)))))
          P))))

(LEMMA
 (^BM^IMPLIES (^BM^ZEROP I)
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^COMP-LIST I A P)) P)
         (^BM^REMAINDER
          (^BM^EXP A
           (^BM^QUOTIENT (^BM^LENGTH (^BM^COMP-LIST I A P))
            (^INT (^BM^CONS (^2) (^BM^ZERO)))))
          P))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^PRIME P) (^BM^LESSP I P))
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^COMP-LIST I A P)) P)
         (^BM^REMAINDER
          (^BM^EXP A
           (^BM^QUOTIENT (^BM^LENGTH (^BM^COMP-LIST I A P))
            (^INT (^BM^CONS (^2) (^BM^ZERO)))))
          P))))

(LEMMA
 (^BM^IMPLIES (^BM^MEMBER X B)
  (EQUAL (^BM^LENGTH (^BM^DELETE X B)) (^BM^SUB1 (^BM^LENGTH B)))))

(LEMMA (^BM^IMPLIES (^BM^PERM A B) (EQUAL (^BM^LENGTH A) (^BM^LENGTH B))))

(LEMMA (EQUAL (^BM^LENGTH (^BM^POSITIVES N)) (^BM^FIX N)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P A)) (^BM^NOT (^BM^RESIDUE A P))))
  (EQUAL (^BM^REMAINDER
          (^BM^EXP A
           (^BM^QUOTIENT (^BM^LENGTH (^BM^COMP-LIST (^BM^SUB1 P) A P))
            (^INT (^BM^CONS (^2) (^BM^ZERO)))))
          P)
         (^BM^SUB1 P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P A)) (^BM^NOT (^BM^RESIDUE A P))))
  (EQUAL (^BM^LENGTH (^BM^COMP-LIST (^BM^SUB1 P) A P)) (^BM^SUB1 P))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP P))
  (EQUAL (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P)
         (^BM^NOT
          (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^SUB1 P))))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P))
  (EQUAL (^BM^QUOTIENT (^BM^SUB1 P) (^INT (^BM^CONS (^2) (^BM^ZERO))))
         (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P))
    (^BM^AND (^BM^NOT (^BM^DIVIDES P A)) (^BM^NOT (^BM^RESIDUE A P)))))
  (EQUAL (^BM^REMAINDER
          (^BM^EXP A (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))) P)
         (^BM^SUB1 P))))

(DEFINE (^BM^RES1 N A P)
 (IF (^BM^ZEROP N)
     (^BM^TRUE)
     (IF (^BM^LESSP (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))
          (^BM^REMAINDER (^BM^TIMES A N) P))
         (^BM^NOT (^BM^RES1 (^BM^SUB1 N) A P))
         (^BM^RES1 (^BM^SUB1 N) A P))))

(DEFINE (^BM^REFLECT X P) (^BM^DIFFERENCE P X))

(DEFINE (^BM^REFLECT-LIST N A P)
 (IF (^BM^ZEROP N)
     (^NIL)
     (IF (^BM^LESSP (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))
          (^BM^REMAINDER (^BM^TIMES A N) P))
         (^BM^CONS (^BM^REFLECT (^BM^REMAINDER (^BM^TIMES A N) P) P)
          (^BM^REFLECT-LIST (^BM^SUB1 N) A P))
         (^BM^CONS (^BM^REMAINDER (^BM^TIMES A N) P)
          (^BM^REFLECT-LIST (^BM^SUB1 N) A P)))))

(LEMMA
 (^BM^IMPLIES (^BM^LEQ B A)
  (EQUAL (^BM^REMAINDER (^BM^DIFFERENCE A (^BM^REMAINDER B P)) P)
         (^BM^REMAINDER (^BM^DIFFERENCE A B) P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^LESSP X P)
   (^BM^AND (^BM^NOT (^BM^ZEROP X)) (^BM^NOT (^BM^ZEROP B))))
  (EQUAL (^BM^REMAINDER (^BM^DIFFERENCE (^BM^TIMES B P) X) P)
         (^BM^DIFFERENCE P X))))

(LEMMA
 (^BM^IMPLIES (^BM^LEQ Y P)
  (EQUAL (^BM^REMAINDER (^BM^TIMES (^BM^REFLECT Y P) X) P)
         (^BM^REMAINDER (^BM^REFLECT (^BM^REMAINDER (^BM^TIMES Y X) P) P) P))))

(LEMMA
 (^BM^IMPLIES (^BM^LEQ Y P)
  (EQUAL (^BM^REMAINDER (^BM^TIMES X (^BM^REFLECT Y P)) P)
         (^BM^REMAINDER (^BM^REFLECT (^BM^REMAINDER (^BM^TIMES X Y) P) P) P))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP N))
  (EQUAL (^BM^REMAINDER
          (^BM^TIMES (^BM^TIMES A N)
           (^BM^TIMES (^BM^EXP A (^BM^SUB1 N)) (^BM^FACT (^BM^SUB1 N))))
          P)
         (^BM^REMAINDER (^BM^TIMES (^BM^EXP A N) (^BM^FACT N)) P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP P))
   (^BM^AND (^BM^NOT (^BM^ZEROP N))
    (^BM^AND
     (^BM^NOT
      (^BM^LESSP (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))
       (^BM^REMAINDER (^BM^TIMES A N) P)))
     (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^REFLECT-LIST (^BM^SUB1 N) A P))
             P)
            (^BM^REMAINDER
             (^BM^TIMES (^BM^EXP A (^BM^SUB1 N)) (^BM^FACT (^BM^SUB1 N)))
             P)))))
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^REFLECT-LIST N A P)) P)
         (^BM^REMAINDER (^BM^TIMES (^BM^EXP A N) (^BM^FACT N)) P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP P))
   (^BM^AND (^BM^NOT (^BM^ZEROP N))
    (^BM^AND
     (^BM^LESSP (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))
      (^BM^REMAINDER (^BM^TIMES A N) P))
     (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^REFLECT-LIST (^BM^SUB1 N) A P))
             P)
            (^BM^REMAINDER
             (^BM^TIMES (^BM^EXP A (^BM^SUB1 N)) (^BM^FACT (^BM^SUB1 N)))
             P)))))
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^REFLECT-LIST N A P)) P)
         (^BM^REMAINDER
          (^BM^REFLECT (^BM^REMAINDER (^BM^TIMES (^BM^EXP A N) (^BM^FACT N)) P)
           P)
          P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP P))
   (^BM^AND (^BM^NOT (^BM^ZEROP N))
    (^BM^AND
     (^BM^NOT
      (^BM^LESSP (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))
       (^BM^REMAINDER (^BM^TIMES A N) P)))
     (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^REFLECT-LIST (^BM^SUB1 N) A P))
             P)
            (^BM^REMAINDER
             (^BM^REFLECT
              (^BM^REMAINDER
               (^BM^TIMES (^BM^EXP A (^BM^SUB1 N)) (^BM^FACT (^BM^SUB1 N))) P)
              P)
             P)))))
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^REFLECT-LIST N A P)) P)
         (^BM^REMAINDER
          (^BM^REFLECT (^BM^REMAINDER (^BM^TIMES (^BM^EXP A N) (^BM^FACT N)) P)
           P)
          P))))

(LEMMA
 (^BM^IMPLIES (^BM^LEQ A P)
  (EQUAL (^BM^REMAINDER (^BM^REFLECT (^BM^REMAINDER (^BM^REFLECT A P) P) P) P)
         (^BM^REMAINDER A P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP P))
   (^BM^AND (^BM^NOT (^BM^ZEROP N))
    (^BM^AND
     (^BM^LESSP (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))
      (^BM^REMAINDER (^BM^TIMES A N) P))
     (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^REFLECT-LIST (^BM^SUB1 N) A P))
             P)
            (^BM^REMAINDER
             (^BM^REFLECT
              (^BM^REMAINDER
               (^BM^TIMES (^BM^EXP A (^BM^SUB1 N)) (^BM^FACT (^BM^SUB1 N))) P)
              P)
             P)))))
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^REFLECT-LIST N A P)) P)
         (^BM^REMAINDER (^BM^TIMES (^BM^EXP A N) (^BM^FACT N)) P))))

(LEMMA
 (^BM^IMPLIES (^BM^ZEROP N)
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^REFLECT-LIST N A P)) P)
         (^BM^REMAINDER (^BM^TIMES (^BM^EXP A N) (^BM^FACT N)) P))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP P))
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^REFLECT-LIST N A P)) P)
         (IF (^BM^RES1 N A P)
             (^BM^REMAINDER (^BM^TIMES (^BM^EXP A N) (^BM^FACT N)) P)
             (^BM^REMAINDER
              (^BM^REFLECT
               (^BM^REMAINDER (^BM^TIMES (^BM^EXP A N) (^BM^FACT N)) P) P)
              P)))))

(LEMMA (EQUAL (^BM^LENGTH (^BM^REFLECT-LIST N A P)) (^BM^FIX N)))

(LEMMA
 (^BM^IMPLIES (^BM^LESSP (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))) X)
  (^BM^NOT
   (^BM^LESSP (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))
    (^BM^REFLECT X P)))))

(LEMMA
 (^BM^ALL-LESSEQP (^BM^REFLECT-LIST N A P)
  (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P) (^BM^AND (^BM^NOT (^BM^DIVIDES P A)) (^BM^LESSP B P)))
  (^BM^ALL-NON-ZEROP (^BM^REFLECT-LIST B A P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^LESSP J I)
    (^BM^AND (^BM^LESSP I P) (^BM^NOT (^BM^DIVIDES P A)))))
  (^BM^NOT
   (EQUAL (^BM^REMAINDER (^BM^TIMES A I) P)
          (^BM^REMAINDER (^BM^TIMES A J) P)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP X)
   (^BM^AND (^BM^NUMBERP Y) (^BM^AND (^BM^LESSP X P) (^BM^LESSP Y P))))
  (EQUAL (EQUAL (^BM^DIFFERENCE P X) (^BM^DIFFERENCE P Y)) (EQUAL X Y))))

(LEMMA (^BM^NUMBERP (^BM^REMAINDER A P)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^LESSP J I)
    (^BM^AND (^BM^LESSP I P) (^BM^NOT (^BM^DIVIDES P A)))))
  (^BM^NOT
   (EQUAL (^BM^REFLECT (^BM^REMAINDER (^BM^TIMES A I) P) P)
          (^BM^REFLECT (^BM^REMAINDER (^BM^TIMES A J) P) P)))))

(LEMMA
 (EQUAL (^BM^REMAINDER (^BM^PLUS (^BM^REMAINDER X P) Y) P)
        (^BM^REMAINDER (^BM^PLUS X Y) P)))

(LEMMA
 (EQUAL (^BM^REMAINDER (^BM^PLUS Y (^BM^REMAINDER X P)) P)
        (^BM^REMAINDER (^BM^PLUS X Y) P)))

(LEMMA
 (^BM^IMPLIES (^BM^AND (EQUAL X (^BM^DIFFERENCE P Y)) (^BM^LESSP Y P))
  (EQUAL (^BM^REMAINDER (^BM^PLUS X Y) P) (^INT (^BM^ZERO)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND
   (EQUAL (^BM^REMAINDER (^BM^TIMES A I) P)
          (^BM^DIFFERENCE P (^BM^REMAINDER (^BM^TIMES A J) P)))
   (^BM^NOT (^BM^ZEROP P)))
  (EQUAL (^BM^REMAINDER (^BM^TIMES A (^BM^PLUS I J)) P) (^INT (^BM^ZERO)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^LEQ I (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
   (^BM^LESSP J I))
  (^BM^AND (^BM^NOT (^BM^ZEROP (^BM^PLUS I J))) (^BM^LESSP (^BM^PLUS I J) P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P A))
    (^BM^AND (^BM^LEQ I (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
     (^BM^LESSP J I))))
  (^BM^NOT
   (EQUAL (^BM^REMAINDER (^BM^TIMES A I) P)
          (^BM^REFLECT (^BM^REMAINDER (^BM^TIMES A J) P) P)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P A))
    (^BM^AND (^BM^LEQ I (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
     (^BM^LESSP J I))))
  (^BM^NOT
   (EQUAL (^BM^REFLECT (^BM^REMAINDER (^BM^TIMES A I) P) P)
          (^BM^REMAINDER (^BM^TIMES A J) P)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P))
    (^BM^AND (^BM^NOT (^BM^DIVIDES P A))
     (^BM^AND (^BM^LEQ I (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
      (^BM^LESSP J I)))))
  (^BM^NOT
   (^BM^MEMBER (^BM^REMAINDER (^BM^TIMES A I) P) (^BM^REFLECT-LIST J A P)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P))
    (^BM^AND (^BM^NOT (^BM^DIVIDES P A))
     (^BM^AND (^BM^LEQ I (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
      (^BM^LESSP J I)))))
  (^BM^NOT
   (^BM^MEMBER (^BM^REFLECT (^BM^REMAINDER (^BM^TIMES A I) P) P)
    (^BM^REFLECT-LIST J A P)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P))
    (^BM^AND (^BM^NOT (^BM^DIVIDES P A))
     (^BM^LEQ I (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))))))
  (^BM^ALL-DISTINCT (^BM^REFLECT-LIST I A P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P))
    (^BM^NOT (^BM^DIVIDES P A))))
  (EQUAL (^BM^TIMES-LIST
          (^BM^REFLECT-LIST (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))
           A P))
         (^BM^FACT (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))))))

(LEMMA
 (EQUAL (^BM^REMAINDER (^BM^PLUS X X) (^INT (^BM^CONS (^2) (^BM^ZERO))))
        (^INT (^BM^ZERO))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP X))
   (^BM^NOT (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P)))
  (^BM^NOT (EQUAL (^BM^REMAINDER (^BM^DIFFERENCE P X) P) X))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P))
    (^BM^AND (^BM^NOT (^BM^DIVIDES P A))
     (^BM^RES1 (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))) A P))))
  (EQUAL (^BM^REMAINDER
          (^BM^EXP A (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))) P)
         (^INT (^BM^CONS (^1) (^BM^ZERO))))))

(LEMMA (^BM^IMPLIES (^BM^LESSP A P) (EQUAL (^BM^REMAINDER A P) (^BM^FIX A))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P))
    (^BM^AND (^BM^NOT (^BM^DIVIDES P A))
     (^BM^NOT
      (^BM^RES1 (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))) A P)))))
  (^BM^NOT
   (EQUAL (^BM^REMAINDER
           (^BM^EXP A (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))) P)
          (^INT (^BM^CONS (^1) (^BM^ZERO)))))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P))
  (^BM^NOT (EQUAL (^BM^SUB1 P) (^INT (^BM^CONS (^1) (^BM^ZERO)))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P A))
    (^BM^NOT (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P))))
  (EQUAL (^BM^RES1 (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))) A P)
         (^BM^RESIDUE A P))))

(DEFINE (^BM^PLUS-LIST L)
 (IF (^BM^NLISTP L)
     (^INT (^BM^ZERO))
     (^BM^PLUS (^BM^CAR L) (^BM^PLUS-LIST (^BM^CDR L)))))

(DEFINE (^BM^QUOT-LIST N A P)
 (IF (^BM^ZEROP N)
     (^NIL)
     (^BM^CONS (^BM^QUOTIENT (^BM^TIMES A N) P)
      (^BM^QUOT-LIST (^BM^SUB1 N) A P))))

(DEFINE (^BM^REM-LIST N A P)
 (IF (^BM^ZEROP N)
     (^NIL)
     (^BM^CONS (^BM^REMAINDER (^BM^TIMES A N) P)
      (^BM^REM-LIST (^BM^SUB1 N) A P))))

(LEMMA
 (EQUAL (^BM^TIMES A (^BM^PLUS-LIST (^BM^POSITIVES N)))
        (^BM^PLUS (^BM^TIMES P (^BM^PLUS-LIST (^BM^QUOT-LIST N A P)))
         (^BM^PLUS-LIST (^BM^REM-LIST N A P)))))

(DEFINE (^BM^EVEN3 X)
 (IF (^BM^ZEROP X) (^BM^TRUE) (^BM^NOT (^BM^EVEN3 (^BM^SUB1 X)))))

(LEMMA (EQUAL (^BM^EVEN3 (^BM^PLUS A B)) (EQUAL (^BM^EVEN3 A) (^BM^EVEN3 B))))

(LEMMA
 (^BM^IMPLIES (^BM^LEQ X P)
  (EQUAL (^BM^EVEN3 (^BM^DIFFERENCE P X)) (EQUAL (^BM^EVEN3 P) (^BM^EVEN3 X)))))

(LEMMA (EQUAL (^BM^EVEN3 (^BM^TIMES A B)) (^BM^OR (^BM^EVEN3 A) (^BM^EVEN3 B))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^EVEN3 P))
  (EQUAL (^BM^EVEN3 (^BM^DIFFERENCE P (^BM^REMAINDER X P)))
         (^BM^NOT (^BM^EVEN3 (^BM^REMAINDER X P))))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^EVEN3 P))
  (EQUAL (^BM^RES1 N A P)
         (^BM^IFF (^BM^EVEN3 (^BM^PLUS-LIST (^BM^REM-LIST N A P)))
          (^BM^EVEN3 (^BM^PLUS-LIST (^BM^REFLECT-LIST N A P)))))))

(LEMMA
 (^BM^IMPLIES (^BM^MEMBER X M)
  (EQUAL (^BM^PLUS X (^BM^PLUS-LIST (^BM^DELETE X M))) (^BM^PLUS-LIST M))))

(LEMMA (^BM^IMPLIES (^BM^PERM L M) (EQUAL (^BM^PLUS-LIST L) (^BM^PLUS-LIST M))))

(LEMMA (EQUAL (^BM^DIVIDES (^INT (^BM^CONS (^2) (^BM^ZERO))) P) (^BM^EVEN3 P)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P A)) (^BM^NOT (^BM^EVEN3 P))))
  (EQUAL (^BM^PLUS-LIST
          (^BM^REFLECT-LIST (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))
           A P))
         (^BM^PLUS-LIST
          (^BM^POSITIVES (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))))))))

(LEMMA (^BM^IMPLIES (EQUAL X Y) (EQUAL (^BM^EVEN3 X) (^BM^EVEN3 Y))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^EVEN3 P))
    (^BM^AND (^BM^NOT (^BM^EVEN3 A)) (^BM^NOT (^BM^DIVIDES P A)))))
  (EQUAL (^BM^RES1 (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))) A P)
         (^BM^EVEN3
          (^BM^PLUS-LIST
           (^BM^QUOT-LIST (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))) A
            P))))))

(DEFINE (^BM^WINS1 X L)
 (IF (^BM^NLISTP L)
     (^INT (^BM^ZERO))
     (IF (^BM^LESSP (^BM^CAR L) X)
         (^BM^ADD1 (^BM^WINS1 X (^BM^CDR L)))
         (^BM^WINS1 X (^BM^CDR L)))))

(DEFINE (^BM^WINS K L)
 (IF (^BM^NLISTP K)
     (^INT (^BM^ZERO))
     (^BM^PLUS (^BM^WINS1 (^BM^CAR K) L) (^BM^WINS (^BM^CDR K) L))))

(DEFINE (^BM^LOSSES1 X L)
 (IF (^BM^NLISTP L)
     (^INT (^BM^ZERO))
     (IF (^BM^LESSP X (^BM^CAR L))
         (^BM^ADD1 (^BM^LOSSES1 X (^BM^CDR L)))
         (^BM^LOSSES1 X (^BM^CDR L)))))

(DEFINE (^BM^LOSSES K L)
 (IF (^BM^NLISTP K)
     (^INT (^BM^ZERO))
     (^BM^PLUS (^BM^LOSSES1 (^BM^CAR K) L) (^BM^LOSSES (^BM^CDR K) L))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^MEMBER X L)) (^BM^ALL-NON-ZEROP L))
  (EQUAL (^BM^PLUS (^BM^LOSSES1 X L) (^BM^WINS1 X L)) (^BM^LENGTH L))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NLISTP (^BM^INTERSECT L M))
   (^BM^AND (^BM^ALL-NON-ZEROP L) (^BM^ALL-NON-ZEROP M)))
  (EQUAL (^BM^PLUS (^BM^WINS L M) (^BM^LOSSES L M))
         (^BM^TIMES (^BM^LENGTH L) (^BM^LENGTH M)))))

(LEMMA (EQUAL (^BM^LOSSES L M) (^BM^WINS M L)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NLISTP (^BM^INTERSECT L M))
   (^BM^AND (^BM^ALL-NON-ZEROP L) (^BM^ALL-NON-ZEROP M)))
  (EQUAL (^BM^PLUS (^BM^WINS L M) (^BM^WINS M L))
         (^BM^TIMES (^BM^LENGTH L) (^BM^LENGTH M)))))

(DEFINE (^BM^MULTS N P)
 (IF (^BM^ZEROP N)
     (^NIL)
     (^BM^CONS (^BM^TIMES N P) (^BM^MULTS (^BM^SUB1 N) P))))

(LEMMA (EQUAL (^BM^LENGTH (^BM^MULTS N P)) (^BM^FIX N)))

(LEMMA
 (^BM^IMPLIES (^BM^LESSP (^BM^TIMES N P) A)
  (^BM^LEQ N (^BM^WINS1 A (^BM^MULTS N P)))))

(LEMMA
 (^BM^IMPLIES (^BM^LEQ N M)
  (^BM^LEQ (^BM^WINS1 A (^BM^MULTS N P)) (^BM^WINS1 A (^BM^MULTS M P)))))

(DEFINE (^BM^QUOT-QUOT-INDUCTION A B C D)
 (IF (^BM^ZEROP B)
     (^BM^TRUE)
     (IF (^BM^ZEROP D)
         (^BM^TRUE)
         (IF (^BM^LESSP A D)
             (^BM^TRUE)
             (IF (^BM^LESSP C B)
                 (^BM^TRUE)
                 (^BM^QUOT-QUOT-INDUCTION (^BM^DIFFERENCE A D) B
                  (^BM^DIFFERENCE C B) D))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP B)) (^BM^LEQ (^BM^TIMES A B) (^BM^TIMES C D)))
  (^BM^LEQ (^BM^QUOTIENT A D) (^BM^QUOTIENT C B))))

(LEMMA
 (^BM^LEQ
  (^BM^QUOTIENT
   (^BM^TIMES (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))) Q) P)
  (^BM^QUOTIENT Q (^INT (^BM^CONS (^2) (^BM^ZERO))))))

(DEFINE (^BM^MONOTONE-QUOT-INDUCTION I J P)
 (IF (^BM^ZEROP P)
     (^BM^TRUE)
     (IF (^BM^LESSP I P)
         (^BM^TRUE)
         (IF (^BM^LESSP J P)
             (^BM^TRUE)
             (^BM^MONOTONE-QUOT-INDUCTION (^BM^DIFFERENCE I P)
              (^BM^DIFFERENCE J P) P)))))

(LEMMA
 (^BM^IMPLIES (^BM^LEQ J I) (^BM^LEQ (^BM^QUOTIENT J P) (^BM^QUOTIENT I P))))

(LEMMA
 (^BM^IMPLIES (^BM^LEQ J (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
  (^BM^LEQ (^BM^QUOTIENT (^BM^TIMES J Q) P)
   (^BM^QUOTIENT Q (^INT (^BM^CONS (^2) (^BM^ZERO)))))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^DIVIDES P X))
  (^BM^LESSP (^BM^TIMES (^BM^QUOTIENT X P) P) X)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P Q))
    (^BM^AND (^BM^NOT (^BM^ZEROP Q))
     (^BM^AND (^BM^NOT (^BM^ZEROP J)) (^BM^LESSP J P)))))
  (^BM^LESSP (^BM^TIMES (^BM^QUOTIENT (^BM^TIMES J Q) P) P) (^BM^TIMES J Q))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P Q))
    (^BM^AND (^BM^LEQ J (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
     (^BM^AND (^BM^NOT (^BM^ZEROP J)) (^BM^NOT (^BM^ZEROP Q))))))
  (^BM^LEQ (^BM^QUOTIENT (^BM^TIMES J Q) P)
   (^BM^WINS1 (^BM^TIMES J Q)
    (^BM^MULTS (^BM^QUOTIENT Q (^INT (^BM^CONS (^2) (^BM^ZERO)))) P)))))

(DEFINE (^BM^WINS2 A N P)
 (IF (^BM^ZEROP N)
     (^INT (^BM^ZERO))
     (IF (^BM^LESSP (^BM^TIMES N P) A) N (^BM^WINS2 A (^BM^SUB1 N) P))))

(LEMMA (^BM^LEQ (^BM^TIMES (^BM^WINS2 A N P) P) A))

(LEMMA (^BM^LEQ (^BM^WINS1 A (^BM^MULTS N P)) N))

(LEMMA (^BM^LEQ (^BM^WINS1 A (^BM^MULTS N P)) (^BM^WINS2 A N P)))

(LEMMA (^BM^LEQ (^BM^TIMES (^BM^WINS1 A (^BM^MULTS N P)) P) A))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP P))
  (^BM^LEQ (^BM^WINS1 A (^BM^MULTS N P)) (^BM^QUOTIENT A P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P Q))
    (^BM^AND (^BM^LEQ J (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
     (^BM^AND (^BM^NOT (^BM^ZEROP J)) (^BM^NOT (^BM^ZEROP Q))))))
  (EQUAL (^BM^WINS1 (^BM^TIMES J Q)
          (^BM^MULTS (^BM^QUOTIENT Q (^INT (^BM^CONS (^2) (^BM^ZERO)))) P))
         (^BM^QUOTIENT (^BM^TIMES J Q) P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P Q))
    (^BM^AND (^BM^NOT (^BM^ZEROP Q))
     (^BM^AND (^BM^NOT (^BM^ZEROP J))
      (^BM^LEQ J (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))))))))
  (EQUAL (^BM^WINS (^BM^MULTS J Q)
          (^BM^MULTS (^BM^QUOTIENT Q (^INT (^BM^CONS (^2) (^BM^ZERO)))) P))
         (^BM^PLUS-LIST (^BM^QUOT-LIST J Q P)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^PRIME Q)
    (^BM^AND (^BM^NOT (EQUAL P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
     (^BM^AND (^BM^NOT (EQUAL Q (^INT (^BM^CONS (^2) (^BM^ZERO)))))
      (^BM^NOT (EQUAL P Q))))))
  (EQUAL (^BM^RES1 (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))) Q P)
         (^BM^RESIDUE Q P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^PRIME Q)
    (^BM^AND (^BM^NOT (EQUAL P Q))
     (^BM^AND (^BM^NOT (EQUAL P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
      (^BM^NOT (EQUAL Q (^INT (^BM^CONS (^2) (^BM^ZERO)))))))))
  (EQUAL (EQUAL (^BM^RESIDUE Q P) (^BM^RESIDUE P Q))
         (^BM^EVEN3
          (^BM^PLUS
           (^BM^PLUS-LIST
            (^BM^QUOT-LIST (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))) Q
             P))
           (^BM^PLUS-LIST
            (^BM^QUOT-LIST (^BM^QUOTIENT Q (^INT (^BM^CONS (^2) (^BM^ZERO)))) P
             Q)))))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP P)) (^BM^ALL-NON-ZEROP (^BM^MULTS N P))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^PRIME Q)
    (^BM^AND (^BM^NOT (EQUAL P Q)) (^BM^AND (^BM^LESSP I Q) (^BM^LESSP J P)))))
  (^BM^NOT (^BM^MEMBER (^BM^TIMES I P) (^BM^MULTS J Q)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^PRIME Q) (^BM^AND (^BM^NOT (EQUAL P Q)) (^BM^LESSP I Q))))
  (^BM^NOT
   (^BM^LISTP
    (^BM^INTERSECT (^BM^MULTS I P)
     (^BM^MULTS (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))) Q))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P) (^BM^AND (^BM^PRIME Q) (^BM^NOT (EQUAL P Q))))
  (EQUAL (^BM^PLUS-LIST
          (^BM^QUOT-LIST (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))) Q
           P))
         (^BM^WINS
          (^BM^MULTS (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))) Q)
          (^BM^MULTS (^BM^QUOTIENT Q (^INT (^BM^CONS (^2) (^BM^ZERO)))) P)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^PRIME Q)
    (^BM^AND (^BM^NOT (EQUAL P Q))
     (^BM^AND (^BM^NOT (EQUAL P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
      (^BM^NOT (EQUAL Q (^INT (^BM^CONS (^2) (^BM^ZERO)))))))))
  (EQUAL (EQUAL (^BM^RESIDUE Q P) (^BM^RESIDUE P Q))
         (^BM^EVEN
          (^BM^TIMES (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))
           (^BM^QUOTIENT Q (^INT (^BM^CONS (^2) (^BM^ZERO)))))))))