Support Nat literals

[flupe]

Currently, Nat literals (when importing the builtin Agda.Builtin.Nat) in terms are desugared into the right sequence of constructor applications.

For patterns, the story is a bit different.

If the literal pattern is 0, then things work out and the pattern is replaced with the zero constructor patterns.

But for other literal Nat patterns, like 3, there's no direct translation to Lambox, as the case construct in Lambox only peels off one layer of constructors.

Two possible solutions:

• There's the EliminateLiteralPatterns treeless transformation, which removes all literal patterns.
  See here.
  But it instead inserts a boolean check over a builtin equality over Nat (or other literals).
  So it requires a builtin ifThenElse and a builtin natEquality, which we don't have out of the box.

The backend could ask for those to be generated as axioms in the Lambox environment, to be supplied when compiling to different targets.

• We could also try to replace a case n {3 -> ...} into successive case applications.

  case n {suc n' -> case n' {suc n'' -> case n'' {suc n'''} -> case n''' { zero -> ... }}}}}.

  However, this generates a lot of extra case branches.
  We need cases to be exhaustive.
  It's unsatisfying.