Library problem

Puzzle: The Monkey and the Coconuts

Five men and a monkey were shipwrecked on a desert island, and they spent the first day gathering coconuts for food. Piled them all up together and went to sleep for the night.
But when they were all asleep one man woke up, and he thought there might be a row about dividing the coconuts in the morning, so he decided to take his share. So he divided the coconuts into five piles. He had one coconut left over, and he gave that to the monkey, and he hid his pile and put the rest all back together.
By and by the next man woke up and did the same thing. And he had one left over, and he gave it to the monkey. And all five of the men did the same thing, one after the other; each one taking a fifth of the coconuts in the pile when he woke up, and each having one left over for the monkey. And in the morning they divided what coconuts were left, and they came out in five equal shares. Of course each one must have known there were coconuts missing; but each one was guilty as the others, so they didn't say anything. How many coconuts were there in the beginning?
Download the Coq source!

Require Import Arith.

Definition wakeUp (coconutsStart : nat) : (Prop × nat) :=
  (coconutsStart mod 5 = 1, 4 × Nat.div (coconutsStart - 1) 5).

Fixpoint iteratedWakeUp (numMen coconutsStart : nat) : Prop := match numMen with
  | 0 ⇒ coconutsStart mod 5 = 0
  | S numMen'let (Pfirst, coconutsNext) := wakeUp coconutsStart in
                 let Prest := iteratedWakeUp numMen' coconutsNext in
                 Pfirst Prest

Definition Puzzle := coconutsStart : nat, iteratedWakeUp 5 coconutsStart.

Theorem Solution : Puzzle.