fun factorial_recursion {n:nat} .<n>. (n : int(n)) : int =
  case+ n of
    | 0 => 1
    | n =>> factorial_recursion(n - 1) * n