欧几里德分裂对自然的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