mutual {
  F : Nat -> Nat
  F Z = (S Z)
  F (S n) = (S n) `minus` M(F(n))

  M : Nat -> Nat
  M Z = Z
  M (S n) = (S n) `minus` F(M(n))
}