task: THEORY
BEGIN
	x: VAR int

	expt_x3: LEMMA x^3 = x*x*x

	divides(n: int, d: int) : bool =
		EXISTS (x: int): n=d*x
	
	div3_theorem: THEOREM
		FORALL (n: nat): 
			(n>2) IMPLIES
				divides(n^3-n, 3)

END task