Unknown Interpretation for "_/_" despite importing Arith

Question

I was trying to write a function to converts a nat to a string in coq. Here is my attempt.

Require Import Arith String.

(*
  append is part of the string library. Its signature is
                 (s1 : string) : string -> string
*)

Fixpoint convert_nat_to_string (n : nat) : string :=
match n with
  | 0 => String "0" EmptyString 
  | 1 => String "1" EmptyString
  | 2 => String "2" EmptyString
  | 3 => String "3" EmptyString
  | 4 => String "4" EmptyString
  | 5 => String "5" EmptyString
  | 6 => String "6" EmptyString
  | 7 => String "7" EmptyString
  | 8 => String "8" EmptyString
  | 9 => String "9" EmptyString
  | _ => (append (convert_nat_to_string (n/10))) (convert_nat_to_string (n mod 10))
end.   

However, on the last branch, coqide gives me an error

Error: Unknown interpretation for notation "_ / _".

even though I have imported the Arith library. Does anyone know why I am getting this error message?

---

Proof that / is part of Arith:

Coq < Require Import Arith.
[Loading ML file z_syntax_plugin.cmxs ... done]
[Loading ML file quote_plugin.cmxs ... done]
[Loading ML file newring_plugin.cmxs ... done]
<W> Grammar extension: in [tactic:simple_tactic], some rule has been masked
<W> Grammar extension: in [tactic:simple_tactic], some rule has been masked
<W> Grammar extension: in [tactic:simple_tactic], some rule has been masked
<W> Grammar extension: in [tactic:simple_tactic], some rule has been masked
<W> Grammar extension: in [tactic:simple_tactic], some rule has been masked

Coq < Check 5/10.
5 / 10
     : nat

Answer 1

As of Coq 8.6, this function is available in Coq.Arith.PeanoNat.

Require Import Coq.Arith.PeanoNat.

Check 10 / 5. (* --> 10 / 5 : nat *)