sigh.v

Definition digit_to_string n : string :=
  match n with
  | 0%Z => "0"
  | 1%Z => "1"
  | 2%Z => "2"
  | 3%Z => "3"
  | 4%Z => "4"
  | 5%Z => "5"
  | 6%Z => "6"
  | 7%Z => "7"
  | 8%Z => "8"
  | 9%Z => "9"
  | _ => ""
  end.

Fixpoint z_to_string' n z acc : string :=
  match n with
  | 0 => acc
  | S n' =>
    let acc' := digit_to_string (Zmod z 10) ++ acc
    in match (Zdiv z 10) with
       | Z0 => acc'
       | z' => z_to_string' n' z' acc'
       end
  end.

Definition z_to_string z :=
  if Z.geb z 0
  then z_to_string' (Z.to_nat z) z ""
  else let z' := Zabs z
       in "-" ++ z_to_string' (Z.to_nat z') z' "".