(* ========================================================================= *)
(* The friendship theorem.                                                   *)
(*                                                                           *)
(* Proof from "Combinatorics Tutorial 2: Friendship Theorem", copyright      *)
(* MathOlymp.com, 2001. Apparently due to J. Q. Longyear and T. D. Parsons.  *)
(* ========================================================================= *)

needs "Library/prime.ml";;
needs "Library/pocklington.ml";;

(* ------------------------------------------------------------------------- *)
(* Useful inductive breakdown principle ending at gcd.                       *)
(* ------------------------------------------------------------------------- *)

let GCD_INDUCT = 
prove
 (`!P. (!m n. P m /\ P (m + n) ==> P n)
       ==> !m n. P m /\ P n ==> P (gcd(m,n))`,

  GEN_TAC THEN STRIP_TAC THEN REPEAT GEN_TAC THEN
  WF_INDUCT_TAC `m + n:num` THEN REPEAT(POP_ASSUM MP_TAC) THEN
  MAP_EVERY (fun t -> SPEC_TAC(t,t)) [`n:num`; `m:num`] THEN
  MATCH_MP_TAC WLOG_LE THEN CONJ_TAC THENL
   [REWRITE_TAC[CONJ_ACI; GCD_SYM; ADD_SYM]; REPEAT STRIP_TAC] THEN
  ASM_CASES_TAC `m = 0` THENL [ASM_MESON_TAC[GCD_0]; ALL_TAC] THEN
  UNDISCH_TAC `!m n:num. P m /\ P (m + n) ==> P n` THEN
  DISCH_THEN(MP_TAC o SPECL [`m:num`; `n - m:num`]) THEN
  ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_SIMP_TAC[SUB_ADD; LT_IMP_LE] THEN
  DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPECL [`m:num`; `n - m:num`]) THEN
  REWRITE_TAC[IMP_IMP] THEN ANTS_TAC THENL
   [ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC;
    ALL_TAC] THEN
  FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LE_EXISTS]) THEN
  DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST_ALL_TAC) THEN
  REWRITE_TAC[ADD_SUB2; GCD_ADD]);;
(* ------------------------------------------------------------------------- *)
(* General theorems about loops in a sequence.                               *)
(* ------------------------------------------------------------------------- *)

let LOOP_GCD = 
prove
 (`!x m n. (!i. x(i + m) = x(i)) /\ (!i. x(i + n) = x(i))
           ==> !i. x(i + gcd(m,n)) = x(i)`,

  GEN_TAC THEN MATCH_MP_TAC GCD_INDUCT THEN MESON_TAC[ADD_AC]);;
let LOOP_COPRIME = 
prove
 (`!x m n. (!i. x(i + m) = x(i)) /\ (!i. x(i + n) = x(i)) /\ coprime(m,n)
           ==> !i. x i = x 0`,

  REPEAT GEN_TAC THEN STRIP_TAC THEN INDUCT_TAC THEN REWRITE_TAC[ADD1] THEN
  ASM_MESON_TAC[LOOP_GCD; COPRIME_GCD]);;
(* ------------------------------------------------------------------------- *)
(* General theorem about partition into equally-sized eqv classes.           *)
(* ------------------------------------------------------------------------- *)

let EQUIVALENCE_UNIFORM_PARTITION = 
prove
 (`!R s k. FINITE s /\
           (!x. x IN s ==> R x x) /\
           (!x y. R x y ==> R y x) /\
           (!x y z. R x y /\ R y z ==> R x z) /\
           (!x:A. x IN s ==> CARD {y | y IN s /\ R x y} = k)
           ==> k divides (CARD s)`,

  REPEAT GEN_TAC THEN
  WF_INDUCT_TAC `CARD(s:A->bool)` THEN
  ASM_CASES_TAC `s:A->bool = {}` THENL
   [ASM_MESON_TAC[CARD_CLAUSES; DIVIDES_0]; REPEAT STRIP_TAC] THEN
  FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
  DISCH_THEN(X_CHOOSE_TAC `a:A`) THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `{y:A | y IN s /\ ~(R (a:A) y)}`) THEN
  REWRITE_TAC[IMP_IMP] THEN ANTS_TAC THENL
   [ASM_SIMP_TAC[IN_ELIM_THM; FINITE_RESTRICT] THEN ASM_REWRITE_TAC[] THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC CARD_PSUBSET THEN
      ASM_SIMP_TAC[PSUBSET; SUBSET; EXTENSION; IN_ELIM_THM] THEN
      ASM_MESON_TAC[];
      GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN
      DISCH_THEN(CONJUNCTS_THEN2 (ANTE_RES_THEN MP_TAC) ASSUME_TAC) THEN
      DISCH_TAC THEN MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
      AP_TERM_TAC THEN ASM SET_TAC[]];
    ALL_TAC] THEN
  DISCH_TAC THEN
  SUBGOAL_THEN `CARD(s) = CARD {y | y IN s /\ (R:A->A->bool) a y} +
                          CARD {y | y IN s /\ ~(R a y)}`
   (fun th -> ASM_SIMP_TAC[th; DIVIDES_ADD; DIVIDES_REFL]) THEN
  CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_UNION_EQ THEN ASM SET_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* With explicit restricted quantification.                                  *)
(* ------------------------------------------------------------------------- *)

let EQUIVALENCE_UNIFORM_PARTITION_RESTRICT = 
prove
 (`!R s k. FINITE s /\
           (!x. x IN s ==> R x x) /\
           (!x y. x IN s /\ y IN s /\ R x y ==> R y x) /\
           (!x y z. x IN s /\ y IN s /\ z IN s /\ R x y /\ R y z ==> R x z) /\
           (!x:A. x IN s ==> CARD {y | y IN s /\ R x y} = k)
           ==> k divides (CARD s)`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC EQUIVALENCE_UNIFORM_PARTITION THEN
  EXISTS_TAC `\x y:A. x IN s /\ y IN s /\ R x y` THEN
  SIMP_TAC[] THEN ASM_REWRITE_TAC[CONJ_ASSOC] THEN ASM_MESON_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* General theorem about pairing up elements of a set.                       *)
(* ------------------------------------------------------------------------- *)

let ELEMENTS_PAIR_UP = 
prove
 (`!s r. FINITE s /\
         (!x. x IN s ==> ~(r x x)) /\
         (!x y. x IN s /\ y IN s /\ r x y ==> r y x) /\
         (!x:A. x IN s ==> ?!y. y IN s /\ r x y)
         ==> EVEN(CARD s)`,

  REPEAT GEN_TAC THEN WF_INDUCT_TAC `CARD(s:A->bool)` THEN
  STRIP_TAC THEN ASM_CASES_TAC `s:A->bool = {}` THEN
  ASM_REWRITE_TAC[CARD_CLAUSES; ARITH] THEN
  FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
  DISCH_THEN(X_CHOOSE_TAC `a:A`) THEN
  MP_TAC(ASSUME `!x:A. x IN s ==> (?!y:A. y IN s /\ r x y)`) THEN
  DISCH_THEN(MP_TAC o SPEC `a:A`) THEN REWRITE_TAC[ASSUME `a:A IN s`] THEN
  DISCH_THEN(MP_TAC o EXISTENCE) THEN
  DISCH_THEN(X_CHOOSE_THEN `b:A` STRIP_ASSUME_TAC) THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `s DELETE (a:A) DELETE b`) THEN
  REWRITE_TAC[IMP_IMP] THEN ANTS_TAC THENL
   [ALL_TAC;
    DISCH_TAC THEN
    SUBGOAL_THEN `s = (a:A) INSERT b INSERT (s DELETE a DELETE b)`
    SUBST1_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
    ASM_SIMP_TAC[CARD_CLAUSES; FINITE_DELETE; FINITE_INSERT] THEN
    REWRITE_TAC[IN_INSERT; IN_DELETE] THEN ASM_MESON_TAC[EVEN]] THEN
  ASM_SIMP_TAC[FINITE_DELETE; IN_DELETE] THEN CONJ_TAC THENL
   [MATCH_MP_TAC CARD_PSUBSET THEN ASM SET_TAC[]; ALL_TAC] THEN
  X_GEN_TAC `x:A` THEN STRIP_TAC THEN
  MP_TAC(ASSUME `!x:A. x IN s ==> (?!y. y IN s /\ r x y)`) THEN
  DISCH_THEN(MP_TAC o SPEC `x:A`) THEN REWRITE_TAC[ASSUME `x:A IN s`] THEN
  MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN
  X_GEN_TAC `y:A` THEN EQ_TAC THEN SIMP_TAC[] THEN ASM_MESON_TAC[]);;
(* ------------------------------------------------------------------------- *)
(* Cycles and paths.                                                         *)
(* ------------------------------------------------------------------------- *)

let cycle = new_definition
 `cycle r k x <=> (!i. r (x i) (x(i + 1))) /\ (!i. x(i + k) = x(i))`;;
let path = new_definition
 `path r k x <=> (!i. i < k ==> r (x i) (x(i + 1))) /\
                 (!i. k < i ==> x(i) = @x. T)`;;
(* ------------------------------------------------------------------------- *)
(* Lemmas about these concepts.                                              *)
(* ------------------------------------------------------------------------- *)

let CYCLE_OFFSET = 
prove
 (`!r k x:num->A. cycle r k x ==> !i m. x(m * k + i) = x(i)`,

  REPEAT GEN_TAC THEN REWRITE_TAC[cycle] THEN STRIP_TAC THEN GEN_TAC THEN
  INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
  ASM_MESON_TAC[ADD_AC]);;
let CYCLE_MOD = 
prove
 (`!r k x:num->A. cycle r k x /\ ~(k = 0) ==> !i. x(i MOD k) = x(i)`,

  MESON_TAC[CYCLE_OFFSET; DIVISION]);;
let PATHS_MONO = 
prove
 (`(!x y. r x y ==> s x y) ==> {x | path r k x} SUBSET {x | path s k x}`,

  REWRITE_TAC[path; IN_ELIM_THM; SUBSET] THEN MESON_TAC[]);;
let HAS_SIZE_PATHS = 
prove
 (`!N m r k. (:A) HAS_SIZE N /\ (!x. {y | r x y} HAS_SIZE m)
             ==> {x:num->A | path r k x} HAS_SIZE (N * m EXP k)`,

  REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
  INDUCT_TAC THEN REWRITE_TAC[EXP; MULT_CLAUSES] THENL
   [SUBGOAL_THEN `{x:num->A | path r 0 x} =
                  IMAGE (\a i. if i = 0 then a else @x. T) (:A)`
    SUBST1_TAC THENL
     [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE; IN_UNIV; path; LT] THEN
      REWRITE_TAC[FUN_EQ_THM; LT_NZ] THEN MESON_TAC[];
      ALL_TAC] THEN
    MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN ASM_REWRITE_TAC[IN_UNIV] THEN
    REWRITE_TAC[FUN_EQ_THM] THEN MESON_TAC[];
    ALL_TAC] THEN
  SUBGOAL_THEN
   `{x:num->A | path r (SUC k) x} =
    IMAGE (\(x,a) i. if i = SUC k then a else x i)
          {x,a | x IN {x | path r k x} /\ a IN {u | r (x k) u}}`
  SUBST1_TAC THENL
   [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE; EXISTS_PAIR_THM] THEN
    X_GEN_TAC `x:num->A` THEN REWRITE_TAC[PAIR_EQ] THEN
    ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c /\ d <=> c /\ d /\ a /\ b`] THEN
    REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
    REWRITE_TAC[FUN_EQ_THM; path; LT] THEN EQ_TAC THENL
     [STRIP_TAC THEN EXISTS_TAC `\i. if i = SUC k then @x. T else x(i):A` THEN
      EXISTS_TAC `x(SUC k):A` THEN SIMP_TAC[] THEN
      CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
      SIMP_TAC[ARITH_RULE `~(k = SUC k) /\ (i < k ==> ~(i = SUC k))`] THEN
      ASM_SIMP_TAC[ADD1; ARITH_RULE `i < k ==> ~(i + 1 = SUC k)`] THEN
      ASM_MESON_TAC[ARITH_RULE `k < i /\ ~(i = k + 1) ==> SUC k < i`];
      ALL_TAC] THEN
    REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
    MAP_EVERY X_GEN_TAC [`z:num->A`; `a:A`] THEN STRIP_TAC THEN
    ASM_REWRITE_TAC[] THEN
    SIMP_TAC[ARITH_RULE `i = k \/ i < k ==> ~(i = SUC k)`] THEN
    REWRITE_TAC[ARITH_RULE `i + 1 = SUC k <=> i = k`] THEN
    ASM_MESON_TAC[ARITH_RULE `SUC k < i ==> ~(i = SUC k) /\ k < i`];
    ALL_TAC] THEN
  ONCE_REWRITE_TAC[ARITH_RULE `N * m * m EXP k = (N * m EXP k) * m`] THEN
  MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
   [REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_PAIR_THM; IN_ELIM_THM] THEN
    REWRITE_TAC[FUN_EQ_THM; path; PAIR_EQ] THEN REPEAT GEN_TAC THEN
    STRIP_TAC THEN CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
    X_GEN_TAC `i:num` THEN ASM_CASES_TAC `i = SUC k` THEN
    ASM_MESON_TAC[ARITH_RULE `k < SUC k`];
    ALL_TAC] THEN
  ASM_SIMP_TAC[HAS_SIZE_PRODUCT_DEPENDENT]);;
let FINITE_PATHS = 
prove
 (`!r k. FINITE(:A) ==> FINITE {x:num->A | path r k x}`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
  EXISTS_TAC `{x:num->A | path (\a b. T) k x}` THEN SIMP_TAC[PATHS_MONO] THEN
  MP_TAC(ISPECL [`CARD(:A)`; `CARD(:A)`; `\a:A b:A. T`; `k:num`]
                HAS_SIZE_PATHS) THEN
  ANTS_TAC THEN ASM_SIMP_TAC[HAS_SIZE; SET_RULE `{y | T} = (:A)`]);;
let HAS_SIZE_CYCLES = 
prove
 (`!r k. FINITE(:A) /\ ~(k = 0)
         ==> {x:num->A | cycle r k x} HAS_SIZE
             CARD{x:num->A | path r k x /\ x(k) = x(0)}`,

  REPEAT STRIP_TAC THEN
  SUBGOAL_THEN
   `{x:num->A | cycle r k x} =
    IMAGE (\x i. x(i MOD k)) {x | path r k x /\ x(k) = x(0)}`
  SUBST1_TAC THENL
   [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM] THEN
    X_GEN_TAC `x:num->A` THEN EQ_TAC THENL
     [DISCH_TAC THEN
      EXISTS_TAC `\i. if i <= k then x(i):A else @x. T` THEN
      REPEAT CONJ_TAC THENL
       [ASM_SIMP_TAC[FUN_EQ_THM; LT_IMP_LE; DIVISION] THEN
        ASM_MESON_TAC[CYCLE_MOD];
        SIMP_TAC[path; LT_IMP_LE] THEN REWRITE_TAC[GSYM NOT_LT] THEN
        SIMP_TAC[ARITH_RULE `i < k ==> ~(k < i + 1)`] THEN
        ASM_MESON_TAC[cycle];
        REWRITE_TAC[LE_0; LE_REFL] THEN ASM_MESON_TAC[cycle; ADD_CLAUSES]];
      REWRITE_TAC[LEFT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
      X_GEN_TAC `y:num->A` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
      REWRITE_TAC[cycle] THEN CONJ_TAC THEN X_GEN_TAC `i:num` THENL
       [ALL_TAC;
        AP_TERM_TAC THEN MATCH_MP_TAC MOD_EQ THEN EXISTS_TAC `1` THEN
        REWRITE_TAC[MULT_CLAUSES]] THEN
      SUBGOAL_THEN `y((i + 1) MOD k):A = y(i MOD k + 1)` SUBST1_TAC THENL
       [ALL_TAC; ASM_MESON_TAC[path; DIVISION]] THEN
      SUBGOAL_THEN `(i + 1) MOD k = (i MOD k + 1) MOD k` SUBST1_TAC THENL
       [MATCH_MP_TAC MOD_EQ THEN EXISTS_TAC `i DIV k` THEN
        REWRITE_TAC[ARITH_RULE `i + 1 = (m + 1) + ik <=> i = ik + m`] THEN
        ASM_MESON_TAC[DIVISION];
        ALL_TAC] THEN
      FIRST_ASSUM(MP_TAC o CONJUNCT2 o SPEC `i:num` o MATCH_MP DIVISION) THEN
      SPEC_TAC(`i MOD k`,`j:num`) THEN GEN_TAC THEN
      ONCE_REWRITE_TAC[ARITH_RULE `j < k <=> j + 1 < k \/ j + 1 = k`] THEN
      STRIP_TAC THEN ASM_SIMP_TAC[MOD_LT] THEN AP_TERM_TAC THEN
      MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `1` THEN
      UNDISCH_TAC `~(k = 0)` THEN ARITH_TAC];
    ALL_TAC] THEN
  MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
   [ALL_TAC;
    REWRITE_TAC[HAS_SIZE] THEN MATCH_MP_TAC FINITE_SUBSET THEN
    EXISTS_TAC `{x:num->A | path r k x}` THEN
    ASM_SIMP_TAC[FINITE_PATHS] THEN SET_TAC[]] THEN
  MAP_EVERY X_GEN_TAC [`x:num->A`; `y:num->A`] THEN SIMP_TAC[IN_ELIM_THM] THEN
  REWRITE_TAC[path; FUN_EQ_THM] THEN STRIP_TAC THEN X_GEN_TAC `i:num` THEN
  REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
   (SPECL [`i:num`; `k:num`] LT_CASES)
  THENL [ASM_MESON_TAC[MOD_LT]; ASM_MESON_TAC[]; ASM_REWRITE_TAC[]] THEN
  ASM_MESON_TAC[MOD_0]);;
let FINITE_CYCLES = 
prove
 (`!r k. FINITE(:A) /\ ~(k = 0) ==> FINITE {x:num->A | cycle r k x}`,

  MESON_TAC[HAS_SIZE_CYCLES; HAS_SIZE]);;
let CARD_PATHCYCLES_STEP = 
prove
 (`!N m r k.
     (:A) HAS_SIZE N /\ ~(k = 0) /\ ~(m = 0) /\
     (!x:A. {y | r x y} HAS_SIZE m) /\
     (!x y. r x y ==> r y x) /\
     (!x y. ~(x = y) ==> ?!z. r x z /\ r z y)
     ==> {x | path r (k + 2) x /\ x(k + 2) = x(0)} HAS_SIZE
         (m * CARD {x | path r k x /\ x(k) = x(0)} +
          CARD {x | path r (k) x /\ ~(x(k) = x(0))})`,

  REPEAT STRIP_TAC THEN
  REWRITE_TAC[SET_RULE
   `{x | path r (k + 2) x /\ x(k + 2) = x(0)} =
    {x | path r (k + 2) x /\ x k = x 0 /\ x(k + 2) = x(0)} UNION
    {x | path r (k + 2) x /\ ~(x k = x 0) /\ x(k + 2) = x(0)}`] THEN
  MATCH_MP_TAC HAS_SIZE_UNION THEN GEN_REWRITE_TAC I [CONJ_ASSOC] THEN
  CONJ_TAC THENL [ALL_TAC; SET_TAC[]] THEN CONJ_TAC THENL
   [SUBGOAL_THEN
     `{x:num->A | path r (k + 2) x /\ x k = x 0 /\ x (k + 2) = x 0} =
      IMAGE (\(x,a) i. if i = k + 1 then a
                     else if i = k + 2 then x(0)
                     else x(i))
            {x,a | x IN {x | path r k x /\ x(k) = x(0)} /\
                   a IN {u | r (x k) u}}`
    SUBST1_TAC THENL
     [ALL_TAC;
      MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
       [REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_PAIR_THM] THEN
        REWRITE_TAC[IN_ELIM_THM; FUN_EQ_THM; PAIR_EQ] THEN
        MAP_EVERY X_GEN_TAC [`y:num->A`; `a:A`; `z:num->A`; `b:A`] THEN
        DISCH_THEN(fun th -> CONJ_TAC THEN MP_TAC th THENL
         [ALL_TAC; MESON_TAC[]]) THEN
        REPEAT(DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN
        DISCH_THEN(fun th -> X_GEN_TAC `i:num` THEN MP_TAC th) THEN
        DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC(SPEC `0` th)) THEN
        REWRITE_TAC[ARITH_RULE `~(0 = k + 1) /\ ~(0 = k + 2)`] THEN
        DISCH_TAC THEN ASM_CASES_TAC `k:num < i` THENL
         [ASM_MESON_TAC[path]; ALL_TAC] THEN
        DISCH_THEN(MP_TAC o SPEC `i:num`) THEN
        ASM_MESON_TAC[ARITH_RULE `k < k + 1 /\ k < k + 2`];
        ALL_TAC] THEN
      ONCE_REWRITE_TAC[MULT_SYM] THEN
      MATCH_MP_TAC HAS_SIZE_PRODUCT_DEPENDENT THEN
      ASM_REWRITE_TAC[] THEN REWRITE_TAC[HAS_SIZE] THEN
      MATCH_MP_TAC FINITE_SUBSET THEN
      EXISTS_TAC `{x:num->A | path r k x}` THEN CONJ_TAC THENL
       [ALL_TAC; SET_TAC[]] THEN
      ASM_MESON_TAC[HAS_SIZE; FINITE_PATHS]] THEN
    REWRITE_TAC[EXTENSION; IN_IMAGE] THEN
    REWRITE_TAC[EXISTS_PAIR_THM; IN_ELIM_PAIR_THM] THEN
    REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN
    X_GEN_TAC `x:num->A` THEN EQ_TAC THENL
     [STRIP_TAC THEN
      EXISTS_TAC `\i. if i <= k then x(i):A else @x. T` THEN
      EXISTS_TAC `(x:num->A) (k + 1)` THEN
      REWRITE_TAC[IN_ELIM_THM; LE_REFL; LE_0] THEN
      ASM_REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
       [ALL_TAC; ASM_MESON_TAC[path; ARITH_RULE `k < k + 2`]] THEN
      CONJ_TAC THENL
       [ALL_TAC;
        UNDISCH_TAC `path r (k + 2) (x:num->A)` THEN
        SIMP_TAC[path; LT_IMP_LE; ARITH_RULE `i < k ==> i + 1 <= k`] THEN
        SIMP_TAC[GSYM NOT_LT] THEN
        MESON_TAC[ARITH_RULE `i < k ==> i < k + 2`]] THEN
      X_GEN_TAC `i:num` THEN
      ASM_CASES_TAC `i = k + 1` THEN ASM_REWRITE_TAC[] THEN
      ASM_CASES_TAC `i = k + 2` THEN ASM_REWRITE_TAC[] THEN
      FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [path]) THEN
      COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
      DISCH_THEN(MP_TAC o SPEC `i:num` o CONJUNCT2) THEN
      ASM_REWRITE_TAC[ARITH_RULE
       `k + 2 < i <=> ~(i <= k) /\ ~(i = k + 1) /\ ~(i = k + 2)`];
      ALL_TAC] THEN
    REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
    MAP_EVERY X_GEN_TAC [`z:num->A`; `b:A`] THEN
    DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
    DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC(SPEC `0` th)) THEN
    REWRITE_TAC[COND_ID; ARITH_RULE `~(0 = k + 1)`] THEN DISCH_TAC THEN
    REWRITE_TAC[CONJ_ASSOC] THEN DISCH_THEN(LABEL_TAC "*") THEN CONJ_TAC THENL
     [ALL_TAC; REMOVE_THEN "*" (MP_TAC o SPEC `k + 2`) THEN
      ASM_REWRITE_TAC[ARITH_RULE `~(k + 2 = k + 1)`]] THEN
    CONJ_TAC THENL
     [ALL_TAC; REMOVE_THEN "*" (MP_TAC o SPEC `k:num`) THEN
      ASM_REWRITE_TAC[ARITH_RULE `~(k = k + 2) /\ ~(k = k + 1)`]] THEN
    UNDISCH_TAC `path r k (z:num->A)` THEN ASM_REWRITE_TAC[path] THEN
    SIMP_TAC[ARITH_RULE
     `k + 2 < i ==> k < i /\ ~(i = k + 1) /\ ~(i = k + 2)`] THEN
    STRIP_TAC THEN X_GEN_TAC `i:num` THEN DISCH_TAC THEN
    ASM_SIMP_TAC[ARITH_RULE `i < k + 2 ==> ~(i = k + 2)`] THEN
    REWRITE_TAC[ARITH_RULE `i + 1 = k + 2 <=> i = k + 1`] THEN
    ASM_CASES_TAC `i = k + 1` THEN ASM_REWRITE_TAC[] THENL
     [ASM_MESON_TAC[ARITH_RULE `~(x + 1 = x)`]; ALL_TAC] THEN
    REWRITE_TAC[EQ_ADD_RCANCEL] THEN COND_CASES_TAC THEN ASM_SIMP_TAC[] THENL
     [ASM_MESON_TAC[]; ALL_TAC] THEN
    ASM_MESON_TAC[ARITH_RULE `i < k + 2 /\ ~(i = k) /\ ~(i = k + 1)
                              ==> i < k`];
    ALL_TAC] THEN
  SUBGOAL_THEN
   `{x:num->A | path r (k + 2) x /\ ~(x k = x 0) /\ x (k + 2) = x 0} =
    IMAGE (\x i. if i = k + 1 then @z. r (x k) z /\ r z (x 0)
               else if i = k + 2 then x(0)
               else x(i))
        {x | path r k x /\ ~(x(k) = x(0))}`
  SUBST1_TAC THENL
   [ALL_TAC;
    MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
     [ALL_TAC;
      REWRITE_TAC[HAS_SIZE] THEN
      MATCH_MP_TAC FINITE_SUBSET THEN
      EXISTS_TAC `{x:num->A | path r k x}` THEN CONJ_TAC THENL
       [ALL_TAC; SET_TAC[]] THEN
      ASM_MESON_TAC[HAS_SIZE; FINITE_PATHS]] THEN
    MAP_EVERY X_GEN_TAC [`x:num->A`; `y:num->A`] THEN
    REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
    REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `i:num` THEN
    ASM_CASES_TAC `k:num < i` THENL
     [ASM_MESON_TAC[path]; ALL_TAC] THEN
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [FUN_EQ_THM]) THEN
    DISCH_THEN(MP_TAC o SPEC `i:num`) THEN
    ASM_MESON_TAC[ARITH_RULE `k < k + 1 /\ k < k + 2`]] THEN
  REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM] THEN
  X_GEN_TAC `x:num->A` THEN REWRITE_TAC[IN_ELIM_THM] THEN EQ_TAC THENL
   [STRIP_TAC THEN
    EXISTS_TAC `\i. if i <= k then x(i):A else @x. T` THEN
    ASM_REWRITE_TAC[LE_REFL; LE_0] THEN CONJ_TAC THENL
     [ALL_TAC;
      UNDISCH_TAC `path r (k + 2) (x:num->A)` THEN
      SIMP_TAC[path; LT_IMP_LE; ARITH_RULE `i < k ==> i + 1 <= k`] THEN
      SIMP_TAC[GSYM NOT_LT] THEN
      MESON_TAC[ARITH_RULE `i < k ==> i < k + 2`]] THEN
    REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `i:num` THEN
    ASM_CASES_TAC `i = k + 1` THEN ASM_REWRITE_TAC[] THENL
     [CONV_TAC SYM_CONV THEN MATCH_MP_TAC SELECT_UNIQUE THEN
      UNDISCH_TAC `path r (k + 2) (x:num->A)` THEN REWRITE_TAC[path] THEN
      DISCH_THEN(MP_TAC o CONJUNCT1) THEN
      DISCH_THEN(fun th -> MP_TAC(SPEC `k:num` th) THEN
                           MP_TAC(SPEC `k + 1` th)) THEN
      REWRITE_TAC[ARITH_RULE `k < k + 2 /\ k + 1 < k + 2`] THEN
      REWRITE_TAC[GSYM ADD_ASSOC; ARITH] THEN ASM_MESON_TAC[];
      ALL_TAC] THEN
    ASM_CASES_TAC `i = k + 2` THEN ASM_REWRITE_TAC[] THEN
    COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
    UNDISCH_TAC `path r (k + 2) (x:num->A)` THEN REWRITE_TAC[path] THEN
    DISCH_THEN(MP_TAC o CONJUNCT2) THEN
    ASM_MESON_TAC[ARITH_RULE `~(i <= k) /\ ~(i = k + 1) /\ ~(i = k + 2)
                              ==> k + 2 < i`];
    ALL_TAC] THEN
  DISCH_THEN(X_CHOOSE_THEN `y:num->A` STRIP_ASSUME_TAC) THEN
  ASM_REWRITE_TAC[ARITH_RULE
   `~(k + 2 = k + 1) /\ ~(0 = k + 1) /\ ~(0 = k + 2) /\ ~(k = k + 1) /\
    ~(k = k + 2)`] THEN
  REWRITE_TAC[path] THEN CONJ_TAC THEN X_GEN_TAC `i:num` THEN DISCH_TAC THENL
   [REWRITE_TAC[ARITH_RULE `i + 1 = k + 2 <=> i = k + 1`] THEN
    ASM_CASES_TAC `i = k + 1` THEN ASM_REWRITE_TAC[] THENL
     [REWRITE_TAC[ARITH_RULE `(k + 1) + 1 = k + 1 <=> F`] THEN ASM_MESON_TAC[];
      ALL_TAC] THEN
    ASM_SIMP_TAC[ARITH_RULE `i < k + 2 ==> ~(i = k + 2)`] THEN
    REWRITE_TAC[EQ_ADD_RCANCEL] THEN COND_CASES_TAC THEN ASM_SIMP_TAC[] THENL
     [ASM_MESON_TAC[]; ALL_TAC] THEN
    UNDISCH_TAC `path r k (y:num->A)` THEN REWRITE_TAC[path] THEN
    DISCH_THEN(MATCH_MP_TAC o CONJUNCT1) THEN
    MAP_EVERY UNDISCH_TAC [`~(i:num = k)`; `~(i = k + 1)`; `i < k + 2`] THEN
    ARITH_TAC;
    ALL_TAC] THEN
  ASM_SIMP_TAC[ARITH_RULE `k + 2 < i ==> ~(i = k + 1) /\ ~(i = k + 2)`] THEN
  ASM_MESON_TAC[path; ARITH_RULE `k + 2 < i ==> k < i`]);;
(* ------------------------------------------------------------------------- *)
(* The first lemma about the number of cycles.                               *)
(* ------------------------------------------------------------------------- *)

let shiftable = new_definition
 `shiftable x y <=> ?k. !i. x(i) = y(i + k)`;;
let SHIFTABLE_REFL = 
prove
 (`!x. shiftable x x`,

  REWRITE_TAC[shiftable] THEN MESON_TAC[ADD_CLAUSES]);;
let SHIFTABLE_TRANS = 
prove
 (`!x y z. shiftable x y /\ shiftable y z ==> shiftable x z`,

  REWRITE_TAC[shiftable] THEN MESON_TAC[ADD_ASSOC]);;
let SHIFTABLE_LOCAL = 
prove
 (`!x y p r. cycle r p x /\ cycle r p y /\ ~(p = 0)
             ==> (shiftable x y <=> ?k. k < p /\ !i. x(i) = y(i + k))`,

  REPEAT STRIP_TAC THEN REWRITE_TAC[shiftable] THEN
  EQ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
  DISCH_THEN(X_CHOOSE_TAC `k:num`) THEN EXISTS_TAC `k MOD p` THEN
  FIRST_ASSUM(MP_TAC o SPEC `k:num` o MATCH_MP DIVISION) THEN
  DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(fun th -> GEN_REWRITE_TAC
   (BINDER_CONV o LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
  ASM_MESON_TAC[CYCLE_OFFSET; ADD_AC]);;
let SHIFTABLE_SYM = 
prove
 (`!x y p r. cycle r p x /\ cycle r p y /\ ~(p = 0) /\ shiftable x y
             ==> shiftable y x`,

  REPEAT GEN_TAC THEN
  ONCE_REWRITE_TAC[TAUT `a /\ b /\ c /\ d <=> (a /\ b /\ c) /\ d`] THEN
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  FIRST_ASSUM(SUBST1_TAC o MATCH_MP SHIFTABLE_LOCAL) THEN
  DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN
  REWRITE_TAC[shiftable] THEN EXISTS_TAC `p - k:num` THEN
  ASM_SIMP_TAC[ARITH_RULE `k < p ==> (i + (p - k)) + k = i + p:num`] THEN
  ASM_MESON_TAC[cycle]);;
let CYCLES_PRIME_LEMMA = 
prove
 (`!r p x. FINITE(:A) /\ prime p /\ (!x. ~(r x x))
           ==> p divides CARD {x:num->A | cycle r p x}`,

  REPEAT GEN_TAC THEN ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[PRIME_0] THEN
  STRIP_TAC THEN MATCH_MP_TAC EQUIVALENCE_UNIFORM_PARTITION_RESTRICT THEN
  EXISTS_TAC `shiftable:(num->A)->(num->A)->bool` THEN
  ASM_SIMP_TAC[IN_ELIM_THM; FINITE_CYCLES] THEN
  CONJ_TAC THENL [MESON_TAC[SHIFTABLE_REFL]; ALL_TAC] THEN
  CONJ_TAC THENL [ASM_MESON_TAC[SHIFTABLE_SYM]; ALL_TAC] THEN
  CONJ_TAC THENL [MESON_TAC[SHIFTABLE_TRANS]; ALL_TAC] THEN
  X_GEN_TAC `x:num->A` THEN DISCH_TAC THEN
  SUBGOAL_THEN `{y:num->A | cycle r p y /\ shiftable x y} HAS_SIZE p`
   (fun th -> MESON_TAC[HAS_SIZE; th]) THEN
  SUBGOAL_THEN `{y:num->A | cycle r p y /\ shiftable x y} =
                IMAGE (\k i. x(i + k)) {k | k < p}`
  SUBST1_TAC THENL
   [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM] THEN
    X_GEN_TAC `y:num->A` THEN REWRITE_TAC[FUN_EQ_THM] THEN EQ_TAC THENL
     [ASM_MESON_TAC[SHIFTABLE_LOCAL; SHIFTABLE_SYM]; ALL_TAC] THEN
    REPEAT STRIP_TAC THENL
     [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [cycle]) THEN
      ASM_REWRITE_TAC[cycle] THEN MESON_TAC[ADD_AC];
      ALL_TAC] THEN
    MATCH_MP_TAC SHIFTABLE_SYM THEN
    MAP_EVERY EXISTS_TAC [`p:num`; `r:A->A->bool`] THEN
    ASM_REWRITE_TAC[] THEN
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [cycle]) THEN
    ASM_REWRITE_TAC[cycle; shiftable] THEN MESON_TAC[ADD_AC];
    ALL_TAC] THEN
  MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN REWRITE_TAC[HAS_SIZE_NUMSEG_LT] THEN
  REWRITE_TAC[IN_ELIM_THM] THEN MATCH_MP_TAC WLOG_LE THEN
  REWRITE_TAC[FUN_EQ_THM] THEN CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
  MAP_EVERY X_GEN_TAC [`k:num`; `l:num`] THEN REPEAT STRIP_TAC THEN
  MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN DISCH_TAC THEN
  SUBGOAL_THEN `!i. x(i):A = x(0)` MP_TAC THENL
   [ALL_TAC; ASM_MESON_TAC[cycle]] THEN
  MATCH_MP_TAC LOOP_COPRIME THEN EXISTS_TAC `p:num` THEN
  REWRITE_TAC[RIGHT_EXISTS_AND_THM] THEN
  CONJ_TAC THENL [ASM_MESON_TAC[cycle]; ALL_TAC] THEN
  EXISTS_TAC `l + (p - k):num` THEN CONJ_TAC THENL
   [X_GEN_TAC `i:num` THEN
    ONCE_REWRITE_TAC[ARITH_RULE `i + l + pk = (i + pk) + l:num`] THEN
    ASSUM_LIST(REWRITE_TAC o map GSYM) THEN
    SIMP_TAC[ARITH_RULE `k < p ==> (i + p - k) + k = i + p:num`;
             ASSUME `k < p:num`] THEN
    ASM_MESON_TAC[cycle];
    ALL_TAC] THEN
  SUBGOAL_THEN `l + p - k = p + l - k:num` SUBST1_TAC THENL
   [MAP_EVERY UNDISCH_TAC [`k < p:num`; `k <= l:num`] THEN ARITH_TAC;
    ALL_TAC] THEN
  REWRITE_TAC[NUMBER_RULE `coprime(p,p + d) <=> coprime(d,p)`] THEN
  MATCH_MP_TAC PRIME_COPRIME_LT THEN
  ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* The theorem itself.                                                       *)
(* ------------------------------------------------------------------------- *)

let FRIENDSHIP = 
prove
 (`!friend:person->person->bool.
      FINITE(:person) /\
      (!x. ~(friend x x)) /\
      (!x y. friend x y ==> friend y x) /\
      (!x y. ~(x = y) ==> ?!z. friend x z /\ friend y z)
      ==> ?u. !v. ~(v = u) ==> friend u v`,

  REPEAT STRIP_TAC THEN UNDISCH_TAC
   `!x y:person. ~(x = y) ==> ?!z:person. friend x z /\ friend y z` THEN
  REWRITE_TAC[EXISTS_UNIQUE_THM] THEN
  REWRITE_TAC[TAUT `a ==> b /\ c <=> (a ==> b) /\ (a ==> c)`] THEN
  REWRITE_TAC[FORALL_AND_THM; RIGHT_IMP_FORALL_THM] THEN
  GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN
  REWRITE_TAC[SKOLEM_THM; IMP_IMP; GSYM CONJ_ASSOC] THEN
  DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
  DISCH_THEN(X_CHOOSE_TAC `mutualfriend:person->person->person`) THEN
  SUBGOAL_THEN `!s:person->bool. FINITE s` ASSUME_TAC THENL
   [ASM_MESON_TAC[SUBSET_UNIV; FINITE_SUBSET]; ALL_TAC] THEN
  ABBREV_TAC `degree = \p:person. CARD {q:person | friend p q}` THEN
  SUBGOAL_THEN `!x y:person. ~(friend x y) ==> degree(x):num <= degree(y)`
  ASSUME_TAC THENL
   [REPEAT STRIP_TAC THEN ASM_CASES_TAC `x:person = y` THENL
     [ASM_MESON_TAC[LE_REFL]; ALL_TAC] THEN
    EXPAND_TAC "degree" THEN MATCH_MP_TAC LE_TRANS THEN
    EXISTS_TAC `CARD(IMAGE (\u. (mutualfriend:person->person->person) u y)
                           {q | friend (x:person) q})` THEN
    CONJ_TAC THENL
     [ALL_TAC; MATCH_MP_TAC CARD_SUBSET THEN ASM SET_TAC[]] THEN
    MATCH_MP_TAC EQ_IMP_LE THEN CONV_TAC SYM_CONV THEN
    MATCH_MP_TAC CARD_IMAGE_INJ THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN
    MAP_EVERY X_GEN_TAC [`u1:person`; `u2:person`] THEN STRIP_TAC THEN
    FIRST_X_ASSUM(MP_TAC o SPECL
     [`x:person`; `(mutualfriend:person->person->person) u1 y`;
      `u1:person`; `u2:person`]) THEN ASM_MESON_TAC[];
    ALL_TAC] THEN
  SUBGOAL_THEN `!x y:person. ~(friend x y) ==> degree x:num = degree y`
  ASSUME_TAC THENL [ASM_MESON_TAC[LE_ANTISYM]; ALL_TAC] THEN
  GEN_REWRITE_TAC I [TAUT `p <=> ~ ~ p`] THEN
  GEN_REWRITE_TAC RAND_CONV [NOT_EXISTS_THM] THEN
  DISCH_THEN(ASSUME_TAC o REWRITE_RULE[NOT_FORALL_THM; NOT_IMP]) THEN
  SUBGOAL_THEN `?m:num. !x:person. degree(x) = m` STRIP_ASSUME_TAC THENL
   [FIRST_ASSUM(X_CHOOSE_THEN `b:person` STRIP_ASSUME_TAC o
      SPEC `a:person`) THEN
    ABBREV_TAC `c = (mutualfriend:person->person->person) a b` THEN
    ABBREV_TAC `k = (degree:person->num) a` THEN EXISTS_TAC `k:num` THEN
    SUBGOAL_THEN `(degree:person->num)(b) = k /\ ~(friend a b) /\
                  friend a c /\ friend b c`
    STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
    SUBGOAL_THEN `!x:person. ~(x = c) ==> degree x = (k:num)` ASSUME_TAC THEN
    ASM_MESON_TAC[];
    ALL_TAC] THEN
  SUBGOAL_THEN `!p:person. {q:person | friend p q} HAS_SIZE m`
  ASSUME_TAC THENL [ASM_MESON_TAC[HAS_SIZE]; ALL_TAC] THEN
  SUBGOAL_THEN `~(m = 0)` ASSUME_TAC THENL
   [DISCH_TAC THEN
    UNDISCH_TAC `!p:person. {q:person | friend p q} HAS_SIZE m` THEN
    ASM_REWRITE_TAC[HAS_SIZE_0; EXTENSION; IN_ELIM_THM; NOT_IN_EMPTY] THEN
    ASM_MESON_TAC[];
    ALL_TAC] THEN
  SUBGOAL_THEN `EVEN(m)` ASSUME_TAC THENL
   [UNDISCH_TAC `!x:person. degree x = (m:num)` THEN
    DISCH_THEN(SUBST1_TAC o SYM o SPEC `a:person`) THEN
    EXPAND_TAC "degree" THEN MATCH_MP_TAC ELEMENTS_PAIR_UP THEN
    EXISTS_TAC `\x y:person. friend a x /\ friend a y /\ friend x y` THEN
    REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[HAS_SIZE];
    ALL_TAC] THEN
  ABBREV_TAC `N = CARD(:person)` THEN
  SUBGOAL_THEN `N = m * (m - 1) + 1` ASSUME_TAC THENL
   [ABBREV_TAC `t = {q:person | friend (a:person) q}` THEN
    SUBGOAL_THEN `FINITE(t:person->bool) /\ CARD t = m` STRIP_ASSUME_TAC THENL
     [ASM_MESON_TAC[HAS_SIZE]; ALL_TAC] THEN
    ABBREV_TAC
     `u = \b:person. {c:person | friend b c /\ ~(c IN (a INSERT t))}` THEN
    EXPAND_TAC "N" THEN
    SUBGOAL_THEN `(:person) = (a INSERT t) UNION UNIONS {u(b) | b IN t}`
    SUBST1_TAC THENL
     [REWRITE_TAC[EXTENSION; IN_INSERT; IN_UNIV; IN_UNION; IN_UNIONS] THEN
      MAP_EVERY EXPAND_TAC ["t";
 "u"] THEN REWRITE_TAC[IN_ELIM_THM] THEN
      X_GEN_TAC `x:person` THEN
      MATCH_MP_TAC(TAUT `(~a /\ ~b ==> c) ==> (a \/ b) \/ c`) THEN
      STRIP_TAC THEN REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
      ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c <=> b /\ a /\ c`] THEN
      ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN REWRITE_TAC[UNWIND_THM2] THEN
      REWRITE_TAC[IN_ELIM_THM; IN_INSERT; DE_MORGAN_THM] THEN
      EXISTS_TAC `mutualfriend (a:person) (x:person) :person` THEN
      EXPAND_TAC "t" THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[];
      ALL_TAC] THEN
    SUBGOAL_THEN `m * (m - 1) + 1 = (m + 1) + m * (m - 2)` SUBST1_TAC THENL
     [SIMP_TAC[ARITH_RULE `a + 1 = (m + 1) + m * c <=> a = m * (1 + c)`] THEN
      AP_TERM_TAC THEN UNDISCH_TAC `EVEN m` THEN
      ASM_CASES_TAC `m = 1` THEN ASM_REWRITE_TAC[ARITH] THEN DISCH_TAC THEN
      MAP_EVERY UNDISCH_TAC [`~(m = 0)`; `~(m = 1)`] THEN ARITH_TAC;
      ALL_TAC] THEN
    SUBGOAL_THEN `m + 1 = CARD((a:person) INSERT t)` SUBST1_TAC THENL
     [ASM_SIMP_TAC[CARD_CLAUSES; ADD1] THEN EXPAND_TAC "t" THEN
      REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[];
      ALL_TAC] THEN
    SUBGOAL_THEN
     `UNIONS {u b :person->bool | (b:person) IN t} HAS_SIZE m * (m - 2)`
    MP_TAC THENL
     [MATCH_MP_TAC HAS_SIZE_UNIONS THEN CONJ_TAC THENL
       [ASM_MESON_TAC[HAS_SIZE]; ALL_TAC] THEN
      CONJ_TAC THENL
       [ALL_TAC;
        EXPAND_TAC "u" THEN REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER] THEN
        REWRITE_TAC[NOT_IN_EMPTY; IN_ELIM_THM; IN_INSERT] THEN
        EXPAND_TAC "t" THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[]] THEN
      REPEAT STRIP_TAC THEN
      MP_TAC(ASSUME `(b:person) IN t`) THEN EXPAND_TAC "t" THEN
      REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC THEN
      SUBGOAL_THEN
       `u (b:person) =
        {q:person | friend q b} DELETE a DELETE (mutualfriend a b)`
      SUBST1_TAC THENL
       [MAP_EVERY EXPAND_TAC ["u"; "t"] THEN
        REWRITE_TAC[EXTENSION; IN_INSERT; IN_DELETE; IN_ELIM_THM] THEN
        X_GEN_TAC `x:person` THEN
        FIRST_X_ASSUM(MP_TAC o SPECL [`a:person`; `b:person`;
         `(mutualfriend:person->person->person) a b`; `x:person`]) THEN
        ASM_MESON_TAC[];
        ALL_TAC] THEN
      ASM_SIMP_TAC[CARD_DELETE; HAS_SIZE] THEN
      REWRITE_TAC[IN_ELIM_THM; IN_DELETE] THEN
      COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
      SUBGOAL_THEN `{q:person | friend q (b:person)} = {q | friend b q}`
      SUBST1_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
      ASM_REWRITE_TAC[ARITH_RULE `m - 1 - 1 = m - 2`] THEN
      ASM_MESON_TAC[HAS_SIZE];
      ALL_TAC] THEN
    REWRITE_TAC[HAS_SIZE] THEN DISCH_THEN(SUBST1_TAC o SYM o CONJUNCT2) THEN
    MATCH_MP_TAC CARD_UNION THEN ASM_REWRITE_TAC[] THEN
    REWRITE_TAC[EXTENSION; IN_INSERT; IN_INTER; NOT_IN_EMPTY; IN_UNIONS] THEN
    REWRITE_TAC[IN_ELIM_THM; LEFT_AND_EXISTS_THM] THEN
    ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c <=> b /\ a /\ c`] THEN
    ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN REWRITE_TAC[UNWIND_THM2] THEN
    MAP_EVERY EXPAND_TAC ["u"; "t"] THEN
    REWRITE_TAC[IN_ELIM_THM; IN_INSERT] THEN ASM_MESON_TAC[];
    ALL_TAC] THEN
  SUBGOAL_THEN `~(m = 2)` ASSUME_TAC THENL
   [DISCH_THEN SUBST_ALL_TAC THEN
    RULE_ASSUM_TAC(CONV_RULE NUM_REDUCE_CONV) THEN
    SUBGOAL_THEN `(:person) HAS_SIZE 3` MP_TAC THENL
     [ASM_REWRITE_TAC[HAS_SIZE]; ALL_TAC] THEN
    CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN REWRITE_TAC[NOT_EXISTS_THM] THEN
    MAP_EVERY X_GEN_TAC [`a:person`; `b:person`; `c:person`] THEN
    REWRITE_TAC[EXTENSION; IN_UNIV; IN_INSERT; NOT_IN_EMPTY] THEN
    STRIP_TAC THEN
    UNDISCH_TAC `!u:person. ?v:person. ~(v = u) /\ ~friend u v` THEN
    REWRITE_TAC[NOT_FORALL_THM; NOT_EXISTS_THM] THEN
    EXISTS_TAC `a:person` THEN
    UNDISCH_TAC `!p:person. {q:person | friend p q} HAS_SIZE 2` THEN
    DISCH_THEN(MP_TAC o SPEC `a:person`) THEN ASM_REWRITE_TAC[] THEN
    CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN
    REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY] THEN
    REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
    MAP_EVERY X_GEN_TAC [`x:person`; `y:person`] THEN
    STRIP_TAC THEN X_GEN_TAC `z:person` THEN
    UNDISCH_TAC `!x:person. x = a \/ x = b \/ x = c` THEN
    DISCH_THEN(fun th -> MAP_EVERY (fun x -> MP_TAC(SPEC x th))
     [`x:person`; `y:person`; `z:person`]) THEN
    ASM_MESON_TAC[];
    ALL_TAC] THEN
  MP_TAC(SPEC `m - 1` PRIME_FACTOR) THEN ANTS_TAC THENL
   [UNDISCH_TAC `~(m = 2)` THEN ARITH_TAC; ALL_TAC] THEN
  DISCH_THEN(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC) THEN
  SUBGOAL_THEN `~(p divides 1)` MP_TAC THENL
   [ASM_MESON_TAC[DIVIDES_ONE; PRIME_1]; ALL_TAC] THEN
  REWRITE_TAC[] THEN
  MATCH_MP_TAC(NUMBER_RULE 
   `!x. p divides (x + 1) /\ p divides x ==> p divides 1`) THEN
  EXISTS_TAC `m - 1` THEN ASM_REWRITE_TAC[] THEN
  ASM_SIMP_TAC[ARITH_RULE `~(m = 0) ==> m - 1 + 1 = m`] THEN
  MATCH_MP_TAC PRIME_DIVEXP THEN EXISTS_TAC `p - 2` THEN
  ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(NUMBER_RULE
   `!q c K1 K2.
        p divides q /\ p divides c /\                
        c = (q + 1) * K1 + K2 /\
        K1 + K2 = ((q + 1) * q + 1) * nep2
        ==> p divides nep2`) THEN
  MAP_EVERY EXISTS_TAC 
   [`m - 1`; `CARD {x:num->person | cycle friend p x}`;
    `CARD {x:num->person | path friend (p-2) x /\ x (p-2) = x 0}`;
    `CARD {x:num->person | path friend (p-2) x /\ ~(x (p-2) = x 0)}`] THEN
  ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
   [MATCH_MP_TAC CYCLES_PRIME_LEMMA THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
  SUBGOAL_THEN `3 <= p` ASSUME_TAC THENL
   [MATCH_MP_TAC(ARITH_RULE `2 <= p /\ ~(p = 2) ==> 3 <= p`) THEN
    ASM_SIMP_TAC[PRIME_GE_2] THEN DISCH_THEN SUBST_ALL_TAC THEN
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM DIVIDES_2]) THEN
    MP_TAC(DIVIDES_CONV `2 divides 1`) THEN REWRITE_TAC[CONTRAPOS_THM] THEN
    MATCH_MP_TAC(NUMBER_RULE
     `!q. t divides q /\ m = q + 1 ==> t divides m ==> t divides w`) THEN
    EXISTS_TAC `m - 1` THEN ASM_REWRITE_TAC[] THEN
    UNDISCH_TAC `~(m = 0)` THEN ARITH_TAC;
    ALL_TAC] THEN
  ASM_SIMP_TAC[ARITH_RULE `~(m = 0) ==> m - 1 + 1 = m`] THEN CONJ_TAC THENL
   [MP_TAC(ISPECL[`friend:person->person->bool`; `p:num`] HAS_SIZE_CYCLES) THEN
    ANTS_TAC THENL [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
    SIMP_TAC[HAS_SIZE] THEN DISCH_THEN(K ALL_TAC) THEN
    MATCH_MP_TAC HAS_SIZE_CARD THEN
    SUBGOAL_THEN `p = (p - 2) + 2` (fun th ->
      GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th])
    THENL [ASM_MESON_TAC[PRIME_GE_2; SUB_ADD]; ALL_TAC] THEN
    MATCH_MP_TAC CARD_PATHCYCLES_STEP THEN EXISTS_TAC `N:num` THEN
    ASM_REWRITE_TAC[] THEN
    CONJ_TAC THENL [ASM_MESON_TAC[HAS_SIZE]; ALL_TAC] THEN
    CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
    UNDISCH_TAC `3 <= p` THEN ARITH_TAC; 
    ALL_TAC] THEN
  MP_TAC(ISPECL [`N:num`; `m:num`; `friend:person->person->bool`; `p - 2`]
               HAS_SIZE_PATHS) THEN
  ANTS_TAC THENL [ASM_MESON_TAC[HAS_SIZE]; ALL_TAC] THEN
  ASM_REWRITE_TAC[HAS_SIZE] THEN
  DISCH_THEN(SUBST1_TAC o SYM o CONJUNCT2) THEN
  MATCH_MP_TAC CARD_UNION_EQ THEN ASM_SIMP_TAC[FINITE_PATHS] THEN SET_TAC[]);;