types - Coq データ型の衝突

Question

Coq で自然数型を再定義して使用しようとすると、次のようになります。

Inductive Nat: Type :=
| O: Nat
| S: Nat -> Nat.

Fixpoint plus (n: Nat) (m: Nat): Nat :=
match n with
    | O => m
    | S n' => S (plus n' m)
end.

Fixpoint mult (n: Nat) (m: Nat): Nat :=
match n with
    | O => O
    | S n' => plus m (mult n' m)
end.

Fixpoint factorial (n: Nat) : Nat :=
match n with
    | O => 1
    | (S n') => mult n (factorial n')
end.

Coq がエラーを出す

「1」という用語は「nat」型を持ちますが、「Nat」型を持つことが期待されます。

私はこの動作の原因を理解しています (実際の数値 '1' は依然として Coq の組み込みの自然数型にマッピングされています) が、それを修正する方法はありますか? ティア。