coq - coq中自然数的欧几里得除法

Question

Coq 标准库中是否有对自然数进行欧几里得除法的功能？我一直找不到。如果没有，那么在数学上是否有理由不应该有一个？

我想要这个的原因是因为我试图将一个列表分成两个较小的列表。我希望一个列表的大小大约是另一个列表的一半，所以我正在计算（长度 xs）/2。

Answer 1

这可能是您正在寻找的：

http://coq.inria.fr/distrib/V8.4/stdlib/Coq.Numbers.Natural.Abstract.NDiv.html

其他欧几里得的东西：

http://coq.inria.fr/distrib/V8.4/stdlib/Coq.Arith.Euclid.html

http://coq.inria.fr/distrib/V8.4/stdlib/Coq.Numbers.NatInt.NZDiv.html

http://coq.inria.fr/distrib/V8.4/stdlib/Coq.ZArith.Zdiv.html

http://coq.inria.fr/distrib/V8.4/stdlib/Coq.ZArith.Zeuclid.html