In Coq you have to name subterms you want to recurse on

boring.v

(*
Fixpoint boringFail (m : nat) : True :=
  match m with
   | S (S m) => boringFail (S m)
   | _       => I
  end.
*)

Fixpoint boringWork (m : nat) : True :=
  match m with
    | S m' => match m' with
               | S m => boringWork m'
               | _   => I
              end
    | _ => I
  end.