factorial : Nat -> Nat
factorial x =
  if x == 0 then 1
  else
    x * fac (Nat.drop x 1)