Defining Mutually Recursive functions in Coq
As stated in Coq Reference Manual (2.3)


  in Fixpoint, the decreasing argument must be given (unless the
  function is not recursive), but it must not necessary be structurally
  decreasing.


Key word is structurally, Coq can't guess, which arguments is decreasing at each step of the recursion.

The reason for this is nicely described in Software Foundations


  Since Coq is not just a functional programming language, but also a
  consistent logic, any potentially non-terminating function needs to be
  rejected. Here is an (invalid!) Coq program showing what would go
  wrong if Coq allowed non-terminating recursive functions:

 Fixpoint loop_false (n : nat) : False := loop_false n. 

  
  That is, propositions like False would become provable (e.g. loop_false 0 would
  be a proof of False), which would be a disaster for Coq's logical
  consistency.