The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

> Theorem Zdiv_eucl_unique :
> forall b q1 q2 r1 r2:Z, b <> 0 ->
>  0 <= r1 < Zabs b -> 0 <= r2 < Zabs b ->
>  b*q1 + r1=b*q2+r2 -> q1=q2/\r1=r2.

Unfortunately I think there is not (the support for the Zdiv is
quite weak at the moment).
There are more theorems in theories/Ints/num/Z/DivModAux.v
Unfortunately we are weaker (only the positive part) :

 Theorem Zdiv_unique:
   forall n d q r, 0 < d -> ( 0 <= r < d ) -> n = d * q + r ->  q = n / d.

 Theorem Zmod_unique:
   forall n d q r, 0 < d -> ( 0 <= r < d ) -> n = d * q + r ->  r = n mod d.

--
Laurent