(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^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^AND (^BM^NOT (^BM^DIVIDES P A)) (^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^COMPLEMENTS I A P)
 (IF (^BM^ZEROP I)
     (^NIL)
     (IF (^BM^MEMBER I (^BM^COMPLEMENTS (^BM^SUB1 I) A P))
         (^BM^COMPLEMENTS (^BM^SUB1 I) A P)
         (^BM^CONS I
          (^BM^CONS (^BM^COMPLEMENT I A P)
           (^BM^COMPLEMENTS (^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^COMPLEMENTS I A P))))

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

(LEMMA (^BM^SUBSETP (^BM^POSITIVES N) (^BM^COMPLEMENTS 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^COMPLEMENTS I A P))))))
  (^BM^MEMBER (^BM^COMPLEMENT J A P) (^BM^COMPLEMENTS 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^COMPLEMENTS I A P))))))))
  (^BM^MEMBER J (^BM^COMPLEMENTS 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^COMPLEMENTS (^BM^SUB1 I) A P))))))
  (^BM^ALL-DISTINCT (^BM^COMPLEMENTS 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^COMPLEMENTS 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^COMPLEMENTS (^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^COMPLEMENTS (^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^COMPLEMENTS (^BM^SUB1 I) A P)))))
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^COMPLEMENTS I A P)) P)
         (^BM^REMAINDER
          (^BM^TIMES A
           (^BM^REMAINDER (^BM^TIMES-LIST (^BM^COMPLEMENTS (^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^COMPLEMENTS (^BM^SUB1 I) A P)))))
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^COMPLEMENTS I A P)) P)
         (^BM^REMAINDER
          (^BM^TIMES A
           (^BM^REMAINDER (^BM^TIMES-LIST (^BM^COMPLEMENTS (^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^COMPLEMENTS (^BM^SUB1 I) A P))))
  (EQUAL (^BM^QUOTIENT (^BM^LENGTH (^BM^COMPLEMENTS I A P))
          (^INT (^BM^CONS (^2) (^BM^ZERO))))
         (^BM^ADD1
          (^BM^QUOTIENT (^BM^LENGTH (^BM^COMPLEMENTS (^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^COMPLEMENTS (^BM^SUB1 I) A P))
             P)
            (^BM^REMAINDER
             (^BM^EXP A
              (^BM^QUOTIENT (^BM^LENGTH (^BM^COMPLEMENTS (^BM^SUB1 I) A P))
               (^INT (^BM^CONS (^2) (^BM^ZERO)))))
             P)))))
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^COMPLEMENTS I A P)) P)
         (^BM^REMAINDER
          (^BM^EXP A
           (^BM^QUOTIENT (^BM^LENGTH (^BM^COMPLEMENTS I A P))
            (^INT (^BM^CONS (^2) (^BM^ZERO)))))
          P))))

(LEMMA
 (^BM^IMPLIES (^BM^ZEROP I)
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^COMPLEMENTS I A P)) P)
         (^BM^REMAINDER
          (^BM^EXP A
           (^BM^QUOTIENT (^BM^LENGTH (^BM^COMPLEMENTS 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^COMPLEMENTS I A P)) P)
         (^BM^REMAINDER
          (^BM^EXP A
           (^BM^QUOTIENT (^BM^LENGTH (^BM^COMPLEMENTS 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^COMPLEMENTS (^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^COMPLEMENTS (^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^EVENP X)
 (IF (^BM^ZEROP X) (^BM^TRUE) (^BM^NOT (^BM^EVENP (^BM^SUB1 X)))))

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

(LEMMA
 (EQUAL (^BM^EVENP (^BM^DIFFERENCE P X))
        (^BM^OR (^BM^LESSP P X) (EQUAL (^BM^EVENP P) (^BM^EVENP X)))))

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

(LEMMA (EQUAL (^BM^EVEN P) (^BM^EVENP P)))

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

(LEMMA
 (EQUAL (^BM^EVEN (^BM^DIFFERENCE P X))
        (^BM^OR (^BM^LESSP P X) (EQUAL (^BM^EVEN P) (^BM^EVEN X)))))

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

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

(LEMMA (EQUAL (^BM^EVEN (^BM^ADD1 X)) (^BM^NOT (^BM^EVEN X))))

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

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P) (^BM^NOT (EQUAL P (^INT (^BM^CONS (^2) (^BM^ZERO))))))
  (^BM^NOT
   (EQUAL (^BM^REMAINDER P (^INT (^BM^CONS (^2) (^BM^ZERO))))
          (^INT (^BM^ZERO))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (EQUAL P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
    (^BM^NOT (^BM^DIVIDES P A))))
  (EQUAL (^BM^REMAINDER
          (^BM^EXP A (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))) P)
         (IF (^BM^RESIDUE A P)
             (^INT (^BM^CONS (^1) (^BM^ZERO)))
             (^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^REFLECTIONS 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^DIFFERENCE P (^BM^REMAINDER (^BM^TIMES A N) P))
          (^BM^REFLECTIONS (^BM^SUB1 N) A P))
         (^BM^CONS (^BM^REMAINDER (^BM^TIMES A N) P)
          (^BM^REFLECTIONS (^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^DIFFERENCE P Y) X) P)
         (^BM^REMAINDER (^BM^DIFFERENCE P (^BM^REMAINDER (^BM^TIMES Y X) P))
          P))))

(LEMMA
 (^BM^IMPLIES (^BM^LEQ Y P)
  (EQUAL (^BM^REMAINDER (^BM^TIMES X (^BM^DIFFERENCE P Y)) P)
         (^BM^REMAINDER (^BM^DIFFERENCE P (^BM^REMAINDER (^BM^TIMES X Y) 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^REFLECTIONS (^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^REFLECTIONS 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^REFLECTIONS (^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^REFLECTIONS N A P)) P)
         (^BM^REMAINDER
          (^BM^DIFFERENCE P
           (^BM^REMAINDER (^BM^TIMES (^BM^EXP A N) (^BM^FACT N)) P))
          P))))

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

(LEMMA
 (^BM^IMPLIES (^BM^LEQ A P)
  (EQUAL (^BM^REMAINDER
          (^BM^DIFFERENCE P (^BM^REMAINDER (^BM^DIFFERENCE P A) 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^REFLECTIONS (^BM^SUB1 N) A P))
             P)
            (^BM^REMAINDER
             (^BM^DIFFERENCE P
              (^BM^REMAINDER
               (^BM^TIMES (^BM^EXP A (^BM^SUB1 N)) (^BM^FACT (^BM^SUB1 N))) P))
             P)))))
  (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST (^BM^REFLECTIONS 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^REFLECTIONS 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^REFLECTIONS 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^DIFFERENCE P
               (^BM^REMAINDER (^BM^TIMES (^BM^EXP A N) (^BM^FACT N)) P))
              P)))))

(LEMMA (EQUAL (^BM^LENGTH (^BM^REFLECTIONS 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^DIFFERENCE P X)))))

(LEMMA
 (^BM^ALL-LESSEQP (^BM^REFLECTIONS 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^REFLECTIONS 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^DIFFERENCE P (^BM^REMAINDER (^BM^TIMES A I) P))
          (^BM^DIFFERENCE P (^BM^REMAINDER (^BM^TIMES A J) 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^DIFFERENCE P (^BM^REMAINDER (^BM^TIMES A 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^DIFFERENCE P (^BM^REMAINDER (^BM^TIMES A I) 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^REFLECTIONS 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^DIFFERENCE P (^BM^REMAINDER (^BM^TIMES A I) P))
    (^BM^REFLECTIONS 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^REFLECTIONS 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^REFLECTIONS (^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 (EQUAL P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
    (^BM^NOT (^BM^DIVIDES P A))))
  (^BM^PERM (^BM^POSITIVES (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
   (^BM^REFLECTIONS (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))) A P))))

(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^MU 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^ADD1 (^BM^MU (^BM^SUB1 N) A P))
         (^BM^MU (^BM^SUB1 N) A P))))

(DEFINE (^BM^GAUSS A P)
 (^BM^EVEN (^BM^MU (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))) A P)))

(LEMMA (EQUAL (^BM^RES1 N A P) (^BM^EVEN (^BM^MU N A P))))

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

(DEFINE (^BM^SUM L)
 (IF (^BM^LISTP L)
     (^BM^PLUS (^BM^CAR L) (^BM^SUM (^BM^CDR L)))
     (^INT (^BM^ZERO))))

(DEFINE (^BM^QUOTIENTS N A P)
 (IF (^BM^ZEROP N)
     (^NIL)
     (^BM^CONS (^BM^QUOTIENT (^BM^TIMES A N) P)
      (^BM^QUOTIENTS (^BM^SUB1 N) A P))))

(DEFINE (^BM^REMAINDERS N A P)
 (IF (^BM^ZEROP N)
     (^NIL)
     (^BM^CONS (^BM^REMAINDER (^BM^TIMES A N) P)
      (^BM^REMAINDERS (^BM^SUB1 N) A P))))

(LEMMA
 (EQUAL (^BM^TIMES A (^BM^SUM (^BM^POSITIVES N)))
        (^BM^PLUS (^BM^TIMES P (^BM^SUM (^BM^QUOTIENTS N A P)))
         (^BM^SUM (^BM^REMAINDERS N A P)))))

(LEMMA
 (EQUAL (^BM^EVEN (^BM^TIMES A (^BM^SUM (^BM^POSITIVES N))))
        (^BM^EVEN
         (^BM^PLUS (^BM^TIMES P (^BM^SUM (^BM^QUOTIENTS N A P)))
          (^BM^SUM (^BM^REMAINDERS N A P))))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^EVEN P))
  (EQUAL (^BM^EVEN (^BM^MU N A P))
         (^BM^IFF (^BM^EVEN (^BM^SUM (^BM^REMAINDERS N A P)))
          (^BM^EVEN (^BM^SUM (^BM^REFLECTIONS N A P)))))))

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

(LEMMA (^BM^IMPLIES (^BM^PERM L M) (EQUAL (^BM^SUM L) (^BM^SUM M))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (EQUAL P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
    (^BM^NOT (^BM^DIVIDES P A))))
  (EQUAL (^BM^SUM
          (^BM^REFLECTIONS (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))) A
           P))
         (^BM^SUM
          (^BM^POSITIVES (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (EQUAL P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
    (^BM^AND (^BM^NOT (^BM^EVEN A)) (^BM^NOT (^BM^DIVIDES P A)))))
  (EQUAL (^BM^GAUSS A P)
         (^BM^EVEN
          (^BM^SUM
           (^BM^QUOTIENTS (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))) A
            P))))))

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

(DEFINE (^BM^W X L)
 (IF (^BM^LISTP L)
     (IF (^BM^LESSP (^BM^CAR L) X)
         (^BM^ADD1 (^BM^W X (^BM^CDR L)))
         (^BM^W X (^BM^CDR L)))
     (^INT (^BM^ZERO))))

(DEFINE (^BM^WINS K L)
 (IF (^BM^LISTP K)
     (^BM^PLUS (^BM^W (^BM^CAR K) L) (^BM^WINS (^BM^CDR K) L))
     (^INT (^BM^ZERO))))

(DEFINE (^BM^ALL-NUMBERP L)
 (IF (^BM^LISTP L)
     (^BM^AND (^BM^NUMBERP (^BM^CAR L)) (^BM^ALL-NUMBERP (^BM^CDR L)))
     (^BM^TRUE)))

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

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

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^MEMBER X L))
   (^BM^AND (^BM^NUMBERP X) (^BM^ALL-NUMBERP L)))
  (EQUAL (^BM^PLUS (^BM^L X L) (^BM^W X L)) (^BM^LENGTH L))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NLISTP (^BM^INTERSECT L M))
   (^BM^AND (^BM^ALL-NUMBERP L) (^BM^ALL-NUMBERP 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-NUMBERP L) (^BM^ALL-NUMBERP 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 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP P)) (^BM^ALL-NUMBERP (^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^NUMBERP N) (EQUAL (^BM^LENGTH (^BM^MULTS N P)) N)))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP P))
  (^BM^LESSP A (^BM^TIMES (^BM^ADD1 (^BM^QUOTIENT A P)) P))))

(LEMMA (^BM^NOT (^BM^LESSP N (^BM^W A (^BM^MULTS N P)))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^LESSP A (^BM^TIMES M P)) (^BM^LEQ M N))
  (^BM^LESSP A (^BM^TIMES N P))))

(LEMMA
 (^BM^IMPLIES (^BM^LESSP A (^BM^TIMES M P))
  (^BM^LESSP (^BM^W A (^BM^MULTS N P)) M)))

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

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

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

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP P))
   (^BM^AND (^BM^NOT (^BM^DIVIDES P A)) (^BM^LEQ (^BM^QUOTIENT A P) N)))
  (^BM^LEQ (^BM^QUOTIENT A P) (^BM^W A (^BM^MULTS N P)))))

(DEFINE (^BM^LQQ-INDUCT 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^LQQ-INDUCT (^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^IMPLIES (^BM^LEQ J A) (^BM^LEQ (^BM^TIMES J Q) (^BM^TIMES A Q))))

(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^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (^BM^DIVIDES P Q))
    (^BM^AND (^BM^NOT (^BM^ZEROP J))
     (^BM^LEQ J (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO))))))))
  (EQUAL (^BM^W (^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^LEQ J (^BM^QUOTIENT P (^INT (^BM^CONS (^2) (^BM^ZERO)))))))
  (EQUAL (^BM^SUM (^BM^QUOTIENTS J Q P))
         (^BM^WINS (^BM^MULTS J Q)
          (^BM^MULTS (^BM^QUOTIENT Q (^INT (^BM^CONS (^2) (^BM^ZERO)))) P)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^PRIME P)
   (^BM^AND (^BM^NOT (EQUAL P (^INT (^BM^CONS (^2) (^BM^ZERO)))))
    (^BM^AND (^BM^PRIME Q)
     (^BM^AND (^BM^NOT (EQUAL Q (^INT (^BM^CONS (^2) (^BM^ZERO)))))
      (^BM^NOT (EQUAL P Q))))))
  (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)))))))))