Arithをインポートしているにもかかわらず "_/_"の解釈が不明

Question

natをstringのcoqに変換する関数を作成しようとしていました。ここに私の試みです。

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. 

しかし、最後の枝に、coqideは私がArithライブラリをインポートしているにもかかわらず、私のエラー

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

を与えます。なぜ誰かがこのエラーメッセージを受け取っているのか分かりませんか？

---

/をArithの一部であることを証明：コック8.6のよう

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

、この関数は、Coq.Arith.PeanoNatで利用可能です。

Require Import Coq.Arith.PeanoNat. 

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