Top-level proof
RW_TAC
[[] |- `!a b. divides a b = ?c. b = a * c`,
[] |- `!p. prime p = ~(p = 1) /\ !x. divides x p ==> (x = 1) \/ (x = p)`]
THEN STP_TAC `~(x = 0) /\ x <= 2` TRIVIAL (ALL_TAC THEN CONV_TAC)
THEN CONJ_TAC THENL
[PROVE_TAC [[] |- `0 * c = 0`, [] |- `~(0 = 2)`], STP_TAC `divides x 2`
TRIVIAL PROVE_TAC
[[] |- `!n. ~(n = 0) ==> !m. divides m n ==> m <= n`, [] |- `~(0 = 2)`]
THEN PROVE_TAC [[] |- `!a b. divides a b = ?c. b = a * c`]]

PROVE_TAC [[] |- `!a b. divides a b = ?c. b = a * c`]
STP_TAC `divides x 2` TRIVIAL PROVE_TAC
[[] |- `!n. ~(n = 0) ==> !m. divides m n ==> m <= n`, [] |- `~(0 = 2)`]

STP_TAC `divides x 2`
PROVE_TAC [[] |- `0 * c = 0`, [] |- `~(0 = 2)`]

REPEAT POP_ASSUM THEN CONV_TAC

CONJ_TAC
STP_TAC `~(x = 0) /\ x <= 2` TRIVIAL (ALL_TAC THEN CONV_TAC)
CONV_TAC
ALL_TAC THEN UNDISCH_TAC `2 = x * c`
UNDISCH_TAC `2 = x * c`
ALL_TAC
UNDISCH_TAC `2 = x * c`
STP_TAC `~(x = 0) /\ x <= 2`
RW_TAC
[[] |- `!a b. divides a b = ?c. b = a * c`,
[] |- `!p. prime p = ~(p = 1) /\ !x. divides x p ==> (x = 1) \/ (x = p)`]

(((((REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN REPEAT NO_TAC) THEN CONV_TAC)
THEN TRY ((COND_CASES_TAC THEN REPEAT COND_CASES_TAC) THEN CONV_TAC))
THEN REPEAT (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic])) THEN REPEAT
(CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC))) THEN TRY
NO_TAC

TRY NO_TAC
NO_TAC ORELSE ALL_TAC
ALL_TAC
STP_TAC `~(x = 0) /\ x <= 2` TRIVIAL (ALL_TAC THEN CONV_TAC)

((((REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN REPEAT NO_TAC) THEN CONV_TAC) THEN TRY
((COND_CASES_TAC THEN REPEAT COND_CASES_TAC) THEN CONV_TAC)) THEN REPEAT
(FIRST [GEN_TAC, CONJ_TAC, UnknownTactic])) THEN REPEAT
(CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC))

REPEAT (CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC))
TRY
(CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC) THEN REPEAT
(CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC)))

(CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC) THEN REPEAT
(CHANGED_TAC (((NO_TAC ORELSE NO_TAC) ORELSE NO_TAC) ORELSE NO_TAC)))
ORELSE ALL_TAC

ALL_TAC
(((REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN REPEAT NO_TAC) THEN CONV_TAC) THEN TRY
((COND_CASES_TAC THEN REPEAT COND_CASES_TAC) THEN CONV_TAC)) THEN REPEAT
(FIRST [GEN_TAC, CONJ_TAC, UnknownTactic])

REPEAT (FIRST [GEN_TAC, CONJ_TAC, UnknownTactic])
TRY
(FIRST [GEN_TAC, CONJ_TAC, UnknownTactic] THEN REPEAT
(FIRST [GEN_TAC, CONJ_TAC, UnknownTactic]))

(FIRST [GEN_TAC, CONJ_TAC, UnknownTactic] THEN REPEAT
(FIRST [GEN_TAC, CONJ_TAC, UnknownTactic])) ORELSE ALL_TAC

((REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN REPEAT NO_TAC) THEN CONV_TAC) THEN TRY
((COND_CASES_TAC THEN REPEAT COND_CASES_TAC) THEN CONV_TAC)

TRY ((COND_CASES_TAC THEN REPEAT COND_CASES_TAC) THEN CONV_TAC)
((COND_CASES_TAC THEN REPEAT COND_CASES_TAC) THEN CONV_TAC) ORELSE ALL_TAC
(REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN REPEAT NO_TAC) THEN CONV_TAC
CONV_TAC
REPEAT (GEN_TAC ORELSE CONJ_TAC) THEN REPEAT NO_TAC

REPEAT (GEN_TAC ORELSE CONJ_TAC)