Euclidean division on naturals in coq

Question

Is there a function for performing euclidean division on naturals in the Coq standard library? I have been unable to find one. If there isn't one, then is there a reason, mathematically, that there shouldn't be one?

The reason I want this is because I am trying to split a list into two smaller lists. I would like one list to be approximately half the size of the other, so I am computing (length xs) / 2.

Answer 1

This might be what you are looking for:

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

Other euclidean things:

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