导入Coq标准库NDiv后无法使用div_unique_exact问题求助

你遇到的问题根源在于：div_unique_exact并不直接在NDiv模块的顶层命名空间里——它被放在了NDiv的子模块NDivFacts中，而默认导入NDiv并不会自动加载这个子模块的内容。

下面给你两种可行的解决办法：

• 方法一：显式导入子模块
  在导入NDiv之后，额外导入NDivFacts子模块，就能直接使用div_unique_exact了：

  Require Import NDiv.
  Require Import NDiv.NDivFacts.
  Check div_unique_exact.
  

• 方法二：使用全称路径引用
  如果不想额外导入子模块，也可以通过完整的模块路径直接引用这个定理：

  Require Import NDiv.
  Check NDiv.NDivFacts.div_unique_exact.
  

补充个小背景：Coq标准库的很多模块会把基础定义和对应的性质定理拆分到不同子模块中，比如NDiv负责提供除法相关的核心定义，NDivFacts则包含这些定义的各类性质证明，所以需要单独导入子模块才能直接访问里面的定理。

内容的提问来源于stack exchange，提问作者Dev