(1) EuclideanDomain gives the definition of Euclidean Domain (ED).
(2) GauInt.EucDomain shows Gaussian Integers form an ED.
(3) Integer.EucDomain2 defines the integer division that allows negative reminder. It gives a more precise estimation of the reminder.
(4) Typeclasses give several typeclasses that help overloading various symbols.
Note:
We use the Agda version 2.6.5, and Agda stdlib verion 2.0 released on Dec 12, 2023.