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