<p>After accepting Vitus' answer, I discovered a different way to accomplish the goal of proving a function terminates in Agda, namely using "sized types."  I am providing my answer here because it seems acceptable, and also for critique of any weak points of this answer.</p>

<p>Sized types are described:
<a href="http://arxiv.org/pdf/1012.4896.pdf">http://arxiv.org/pdf/1012.4896.pdf</a></p>

<p>They are implemented in Agda, not only MiniAgda; see here: <a href="http://www2.tcs.ifi.lmu.de/~abel/talkAIM2008Sendai.pdf">http://www2.tcs.ifi.lmu.de/~abel/talkAIM2008Sendai.pdf</a>.</p>

<p>The idea is to augment the data type with a size that allows the typechecker to more easily prove termination.  Size is defined in the standard library.</p>

<pre><code>open import Size
</code></pre>

<p>We define sized natural numbers:</p>

<pre><code>data Nat : {i : Size} \to Set where
    zero : {i : Size} \to Nat {\up i} 
    succ : {i : Size} \to Nat {i} \to Nat {\up i}
</code></pre>

<p>Next, we define predecessor and subtraction (monus):</p>

<pre><code>pred : {i : Size} → Nat {i} → Nat {i}
pred .{↑ i} (zero {i}) = zero {i}
pred .{↑ i} (succ {i} n) = n 

sub : {i : Size} → Nat {i} → Nat {∞} → Nat {i}
sub .{↑ i} (zero {i}) n = zero {i}
sub .{↑ i} (succ {i} m) zero = succ {i} m
sub .{↑ i} (succ {i} m) (succ n) = sub {i} m n
</code></pre>

<p>Now, we may define division via Euclid's algorithm:</p>

<pre><code>div : {i : Size} → Nat {i} → Nat → Nat {i}
div .{↑ i} (zero {i}) n = zero {i}
div .{↑ i} (succ {i} m) n = succ {i} (div {i} (sub {i} m n) n)

data ⊥ : Set where
record ⊤ : Set where
notZero :  Nat → Set
notZero zero = ⊥
notZero _ = ⊤
</code></pre>

<p>We give division for nonzero denominators.
If the denominator is nonzero, then it is of the form, b+1.  We then do
divPos a (b+1) = div a b 
Since div a b returns ceiling (a/(b+1)).</p>

<pre><code>divPos : {i : Size} → Nat {i} → (m : Nat) → (notZero m) → Nat {i}
divPos a (succ b) p = div a b
divPos a zero ()
</code></pre>

<p>As auxiliary:</p>

<pre><code>div2 : {i : Size} → Nat {i} → Nat {i}
div2 n = divPos n (succ (succ zero)) (record {})
</code></pre>

<p>Now we can define a divide and conquer method for computing the n-th Fibonacci number.</p>

<pre><code>fibd : {i : Size} → Nat {i} → Nat
fibd zero = zero
fibd (succ zero) = succ zero
fibd (succ (succ zero)) = succ zero
fibd (succ n) with even (succ n)
fibd .{↑ i}  (succ {i} n) | true = 
  let
    -- When m=n+1, the input, is even, we set k = m/2
    -- Note, ceil(m/2) = ceil(n/2)
    k = div2 {i} n
    fib[k-1] = fibd {i} (pred {i} k)
    fib[k] = fibd {i} k
    fib[k+1] =  fib[k-1] + fib[k]
  in
    (fib[k+1] * fib[k]) + (fib[k] * fib[k-1])
fibd .{↑ i} (succ {i} n) | false = 
  let
    -- When m=n+1, the input, is odd, we set k = n/2 = (m-1)/2.
    k = div2 {i} n
    fib[k-1] = fibd {i} (pred {i} k)
    fib[k] = fibd {i} k
    fib[k+1] = fib[k-1] + fib[k]
  in
    (fib[k+1] * fib[k+1]) + (fib[k] * fib[k])
</code></pre>
Assisting Agda's termination checker
<p>Suppose we define a function</p>

<pre><code>f : N \to N
f 0 = 0
f (s n) = f (n/2) -- this / operator is implemented as floored division.
</code></pre>

<p>Agda will paint f in salmon because it cannot tell if n/2 is smaller than n.  I don't know how to tell Agda's termination checker anything.  I see in the standard library they have a floored division by 2 and a proof that n/2 &lt; n.  However, I still fail to see how to get the termination checker to realize that recursion has been made on a smaller subproblem.</p>