Fixpoint stringOfNatAux (time n : nat) (acc : string) : string :=
  let acc' := String (digitOfNat (n mod 10)) acc in
  match time with
  | 0 => acc'
  | S time' =>
    match n / 10 with
    | 0 => acc'
    | n' => stringOfNatAux time' n' acc'
    end
  end.
